[{"volume":4202,"publication_status":"published","date_created":"2018-12-11T12:08:49Z","doi":"10.1007/11867340_1","citation":{"mla":"Henzinger, Thomas A., and Vinayak Prabhu. <i>Timed Alternating-Time Temporal Logic</i>. Vol. 4202, Springer, 2006, pp. 1–17, doi:<a href=\"https://doi.org/10.1007/11867340_1\">10.1007/11867340_1</a>.","short":"T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17.","ista":"Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.","ieee":"T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, vol. 4202, pp. 1–17.","apa":"Henzinger, T. A., &#38; Prabhu, V. (2006). Timed alternating-time temporal logic (Vol. 4202, pp. 1–17). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. <a href=\"https://doi.org/10.1007/11867340_1\">https://doi.org/10.1007/11867340_1</a>","chicago":"Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal Logic,” 4202:1–17. Springer, 2006. <a href=\"https://doi.org/10.1007/11867340_1\">https://doi.org/10.1007/11867340_1</a>.","ama":"Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202. Springer; 2006:1-17. doi:<a href=\"https://doi.org/10.1007/11867340_1\">10.1007/11867340_1</a>"},"extern":1,"quality_controlled":0,"alternative_title":["LNCS"],"status":"public","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Prabhu","full_name":"Prabhu, Vinayak S","first_name":"Vinayak"}],"date_published":"2006-09-19T00:00:00Z","day":"19","publisher":"Springer","publist_id":"296","abstract":[{"text":"We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.","lang":"eng"}],"conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"_id":"4432","type":"conference","date_updated":"2021-01-12T07:56:56Z","title":"Timed alternating-time temporal logic","page":"1 - 17","month":"09","year":"2006","acknowledgement":"This research was supported in part by the NSF grants CCR-0208875, CCR-0225610, and CCR-0234690.","intvolume":"      4202"},{"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Matic","full_name":"Matic, Slobodan","first_name":"Slobodan"}],"status":"public","quality_controlled":0,"citation":{"ieee":"T. A. Henzinger and S. Matic, “An interface algebra for real-time components,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, 2006, pp. 253–266.","ista":"Henzinger TA, Matic S. 2006. An interface algebra for real-time components. RTAS: Real-time and Embedded Technology and Applications Symposium, 253–266.","short":"T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266.","mla":"Henzinger, Thomas A., and Slobodan Matic. <i>An Interface Algebra for Real-Time Components</i>. IEEE, 2006, pp. 253–66, doi:<a href=\"https://doi.org/10.1109/RTAS.2006.11\">10.1109/RTAS.2006.11</a>.","ama":"Henzinger TA, Matic S. An interface algebra for real-time components. In: IEEE; 2006:253-266. doi:<a href=\"https://doi.org/10.1109/RTAS.2006.11\">10.1109/RTAS.2006.11</a>","chicago":"Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time Components,” 253–66. IEEE, 2006. <a href=\"https://doi.org/10.1109/RTAS.2006.11\">https://doi.org/10.1109/RTAS.2006.11</a>.","apa":"Henzinger, T. A., &#38; Matic, S. (2006). An interface algebra for real-time components (pp. 253–266). Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, IEEE. <a href=\"https://doi.org/10.1109/RTAS.2006.11\">https://doi.org/10.1109/RTAS.2006.11</a>"},"extern":1,"date_created":"2018-12-11T12:08:50Z","publication_status":"published","doi":"10.1109/RTAS.2006.11","publist_id":"294","abstract":[{"text":"We present an assume-guarantee interface algebra for real-time components. In our formalism a component implements a set of task sequences that share a resource. A component interface consists of an arrival rate function and a latency for each task sequence, and a capacity function for the shared resource. The interface specifies that the component guarantees certain task latencies depending on assumptions about task arrival rates and allocated resource capacities. Our algebra defines compatibility and refinement relations on interfaces. Interface compatibility can be checked on partial designs, even when some component interfaces are yet unknown. In this case interface composition computes as new assumptions the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. Interface refinement is defined in a way that ensures that compatible interfaces can be refined and implemented independently. Our algebra thus formalizes an interface-based design methodology that supports both the incremental addition of new components and the independent stepwise refinement of existing components. We demonstrate the flexibility and efficiency of the framework through simulation experiments.","lang":"eng"}],"date_published":"2006-04-24T00:00:00Z","publisher":"IEEE","day":"24","title":"An interface algebra for real-time components","conference":{"name":"RTAS: Real-time and Embedded Technology and Applications Symposium"},"date_updated":"2021-01-12T07:56:57Z","_id":"4436","type":"conference","month":"04","year":"2006","page":"253 - 266"},{"abstract":[{"text":"The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.","lang":"eng"}],"publist_id":"295","day":"20","publisher":"Springer","date_published":"2006-09-20T00:00:00Z","extern":1,"citation":{"mla":"Henzinger, Thomas A., and Nir Piterman. <i>Solving Games without Determinization</i>. Vol. 4207, Springer, 2006, pp. 395–410, doi:<a href=\"https://doi.org/10.1007/11874683_26\">10.1007/11874683_26</a>.","short":"T.A. Henzinger, N. Piterman, in:, Springer, 2006, pp. 395–410.","ieee":"T. A. Henzinger and N. Piterman, “Solving games without determinization,” presented at the CSL: Computer Science Logic, 2006, vol. 4207, pp. 395–410.","ista":"Henzinger TA, Piterman N. 2006. Solving games without determinization. CSL: Computer Science Logic, LNCS, vol. 4207, 395–410.","chicago":"Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization,” 4207:395–410. Springer, 2006. <a href=\"https://doi.org/10.1007/11874683_26\">https://doi.org/10.1007/11874683_26</a>.","apa":"Henzinger, T. A., &#38; Piterman, N. (2006). Solving games without determinization (Vol. 4207, pp. 395–410). Presented at the CSL: Computer Science Logic, Springer. <a href=\"https://doi.org/10.1007/11874683_26\">https://doi.org/10.1007/11874683_26</a>","ama":"Henzinger TA, Piterman N. Solving games without determinization. In: Vol 4207. Springer; 2006:395-410. doi:<a href=\"https://doi.org/10.1007/11874683_26\">10.1007/11874683_26</a>"},"quality_controlled":0,"alternative_title":["LNCS"],"author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"last_name":"Piterman","full_name":"Piterman, Nir","first_name":"Nir"}],"status":"public","doi":"10.1007/11874683_26","volume":4207,"publication_status":"published","date_created":"2018-12-11T12:08:51Z","intvolume":"      4207","acknowledgement":"This research was supported in part by the Swiss National Science Foundation.","year":"2006","month":"09","page":"395 - 410","title":"Solving games without determinization","type":"conference","_id":"4437","date_updated":"2021-01-12T07:56:58Z","conference":{"name":"CSL: Computer Science Logic"}},{"type":"journal_article","_id":"4451","date_updated":"2021-01-12T07:57:04Z","title":"On the universal and existential fragments of the mu-calculus","page":"173 - 186","issue":"2","year":"2006","intvolume":"       354","month":"03","doi":"10.1016/j.tcs.2005.11.015","volume":354,"publication_status":"published","date_created":"2018-12-11T12:08:55Z","citation":{"ieee":"T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential fragments of the mu-calculus,” <i>Theoretical Computer Science</i>, vol. 354, no. 2. Elsevier, pp. 173–186, 2006.","ista":"Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.","short":"T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354 (2006) 173–186.","mla":"Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of the Mu-Calculus.” <i>Theoretical Computer Science</i>, vol. 354, no. 2, Elsevier, 2006, pp. 173–86, doi:<a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">10.1016/j.tcs.2005.11.015</a>.","ama":"Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments of the mu-calculus. <i>Theoretical Computer Science</i>. 2006;354(2):173-186. doi:<a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">10.1016/j.tcs.2005.11.015</a>","chicago":"Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal and Existential Fragments of the Mu-Calculus.” <i>Theoretical Computer Science</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">https://doi.org/10.1016/j.tcs.2005.11.015</a>.","apa":"Henzinger, T. A., Kupferman, O., &#38; Majumdar, R. (2006). On the universal and existential fragments of the mu-calculus. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2005.11.015\">https://doi.org/10.1016/j.tcs.2005.11.015</a>"},"extern":1,"status":"public","quality_controlled":0,"author":[{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Orna","full_name":"Kupferman, Orna","last_name":"Kupferman"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar S","first_name":"Ritankar"}],"publisher":"Elsevier","day":"28","publication":"Theoretical Computer Science","date_published":"2006-03-28T00:00:00Z","abstract":[{"text":"One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternation-free fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.","lang":"eng"}],"publist_id":"276"},{"publist_id":"206","abstract":[{"lang":"eng","text":"We consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi."}],"date_published":"2006-01-01T00:00:00Z","day":"01","publisher":"ACM","citation":{"ista":"Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A new algorithm for property checking. FSE: Foundations of Software Engineering, 117–127.","ieee":"B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy: A new algorithm for property checking,” presented at the FSE: Foundations of Software Engineering, 2006, pp. 117–127.","short":"B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006, pp. 117–127.","mla":"Gulavani, Bhargav, et al. <i>Synergy: A New Algorithm for Property Checking</i>. ACM, 2006, pp. 117–27, doi:<a href=\"https://doi.org/10.1145/1181775.1181790\">10.1145/1181775.1181790</a>.","ama":"Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm for property checking. In: ACM; 2006:117-127. doi:<a href=\"https://doi.org/10.1145/1181775.1181790\">10.1145/1181775.1181790</a>","apa":"Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., &#38; Rajamani, S. (2006). Synergy: A new algorithm for property checking (pp. 117–127). Presented at the FSE: Foundations of Software Engineering, ACM. <a href=\"https://doi.org/10.1145/1181775.1181790\">https://doi.org/10.1145/1181775.1181790</a>","chicago":"Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM, 2006. <a href=\"https://doi.org/10.1145/1181775.1181790\">https://doi.org/10.1145/1181775.1181790</a>."},"extern":1,"quality_controlled":0,"author":[{"last_name":"Gulavani","full_name":"Gulavani, Bhargav S","first_name":"Bhargav"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Yamini","full_name":"Kannan, Yamini","last_name":"Kannan"},{"last_name":"Nori","first_name":"Aditya","full_name":"Nori, Aditya V"},{"full_name":"Rajamani, Sriram K","first_name":"Sriram","last_name":"Rajamani"}],"status":"public","date_created":"2018-12-11T12:09:18Z","publication_status":"published","doi":"10.1145/1181775.1181790","month":"01","year":"2006","page":"117 - 127","title":"Synergy: A new algorithm for property checking","conference":{"name":"FSE: Foundations of Software Engineering"},"_id":"4523","type":"conference","date_updated":"2021-01-12T07:59:26Z"},{"page":"132 - 141","year":"2006","month":"01","_id":"4526","type":"conference","date_updated":"2021-01-12T07:59:27Z","conference":{"name":"EMSOFT: Embedded Software "},"title":"A hierarchical coordination language for interacting real-time tasks","day":"01","publisher":"ACM","date_published":"2006-01-01T00:00:00Z","abstract":[{"text":"We designed and implemented a new programming language called Hierarchical Timing Language (HTL) for hard realtime systems. Critical timing constraints are specified within the language,and ensured by the compiler. Programs in HTL are extensible in two dimensions without changing their timing behavior: new program modules can be added, and individual program tasks can be refined. The mechanism supporting time invariance under parallel composition is that different program modules communicate at specified instances of time. Time invariance under refinement is achieved by conservative scheduling of the top level. HTL is a coordination language, in that individual tasks can be implemented in &quot;foreign&quot; languages. As a case study, we present a distributed HTL implementation of an automotive steer-by-wire controller.","lang":"eng"}],"publist_id":"201","doi":"10.1145/1176887.1176907","date_created":"2018-12-11T12:09:18Z","publication_status":"published","extern":1,"citation":{"ama":"Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. A hierarchical coordination language for interacting real-time tasks. In: ACM; 2006:132-141. doi:<a href=\"https://doi.org/10.1145/1176887.1176907\">10.1145/1176887.1176907</a>","chicago":"Ghosal, Arkadeb, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, and Alberto Sangiovanni Vincentelli. “A Hierarchical Coordination Language for Interacting Real-Time Tasks,” 132–41. ACM, 2006. <a href=\"https://doi.org/10.1145/1176887.1176907\">https://doi.org/10.1145/1176887.1176907</a>.","apa":"Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., &#38; Sangiovanni Vincentelli, A. (2006). A hierarchical coordination language for interacting real-time tasks (pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. <a href=\"https://doi.org/10.1145/1176887.1176907\">https://doi.org/10.1145/1176887.1176907</a>","ieee":"A. Ghosal, T. A. Henzinger, D. Iercan, C. Kirsch, and A. Sangiovanni Vincentelli, “A hierarchical coordination language for interacting real-time tasks,” presented at the EMSOFT: Embedded Software , 2006, pp. 132–141.","ista":"Ghosal A, Henzinger TA, Iercan D, Kirsch C, Sangiovanni Vincentelli A. 2006. A hierarchical coordination language for interacting real-time tasks. EMSOFT: Embedded Software , 132–141.","mla":"Ghosal, Arkadeb, et al. <i>A Hierarchical Coordination Language for Interacting Real-Time Tasks</i>. ACM, 2006, pp. 132–41, doi:<a href=\"https://doi.org/10.1145/1176887.1176907\">10.1145/1176887.1176907</a>.","short":"A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli, in:, ACM, 2006, pp. 132–141."},"author":[{"last_name":"Ghosal","first_name":"Arkadeb","full_name":"Ghosal, Arkadeb"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"last_name":"Iercan","first_name":"Daniel","full_name":"Iercan, Daniel"},{"full_name":"Kirsch, Christoph M","first_name":"Christoph","last_name":"Kirsch"},{"first_name":"Alberto","full_name":"Sangiovanni-Vincentelli, Alberto","last_name":"Sangiovanni Vincentelli"}],"quality_controlled":0,"status":"public"},{"publisher":"IEEE","day":"03","date_published":"2006-12-03T00:00:00Z","abstract":[{"lang":"eng","text":"Computational modeling of biological systems is becoming increasingly common as scientists attempt to understand biological phenomena in their full complexity. Here we distinguish between two types of biological models mathematical and computational - according to their different representations of biological phenomena and their diverse potential. We call the approach of constructing computational models of biological systems executable biology, as it focuses on the design of executable computer algorithms that mimic biological phenomena. We give an overview of the main modeling efforts in this direction, and discuss some of the new challenges that executable biology poses for computer science and biology. We argue that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research, driving biology towards a more precise engineering discipline."}],"publist_id":"197","doi":"10.1109/WSC.2006.322942","date_created":"2018-12-11T12:09:19Z","publication_status":"published","status":"public","quality_controlled":0,"author":[{"last_name":"Fisher","first_name":"Jasmin","full_name":"Fisher, Jasmin"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"}],"extern":1,"citation":{"apa":"Fisher, J., &#38; Henzinger, T. A. (2006). Executable biology (pp. 1675–1682). Presented at the WSC: Winter Simulation Conference, IEEE. <a href=\"https://doi.org/10.1109/WSC.2006.322942\">https://doi.org/10.1109/WSC.2006.322942</a>","chicago":"Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82. IEEE, 2006. <a href=\"https://doi.org/10.1109/WSC.2006.322942\">https://doi.org/10.1109/WSC.2006.322942</a>.","ama":"Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:<a href=\"https://doi.org/10.1109/WSC.2006.322942\">10.1109/WSC.2006.322942</a>","short":"J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682.","mla":"Fisher, Jasmin, and Thomas A. Henzinger. <i>Executable Biology</i>. IEEE, 2006, pp. 1675–82, doi:<a href=\"https://doi.org/10.1109/WSC.2006.322942\">10.1109/WSC.2006.322942</a>.","ieee":"J. Fisher and T. A. Henzinger, “Executable biology,” presented at the WSC: Winter Simulation Conference, 2006, pp. 1675–1682.","ista":"Fisher J, Henzinger TA. 2006. Executable biology. WSC: Winter Simulation Conference, 1675–1682."},"page":"1675 - 1682","year":"2006","month":"12","date_updated":"2021-01-12T07:59:28Z","type":"conference","_id":"4528","conference":{"name":"WSC: Winter Simulation Conference"},"title":"Executable biology"},{"page":"512 - 523","intvolume":"      3884","year":"2006","month":"02","type":"conference","_id":"4538","date_updated":"2021-01-12T07:59:32Z","conference":{"name":"STACS: Theoretical Aspects of Computer Science"},"title":"Strategy improvement and randomized subexponential algorithms for stochastic parity games","publisher":"Springer","day":"14","date_published":"2006-02-14T00:00:00Z","abstract":[{"lang":"eng","text":"A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy improvement algorithm for stochastic parity games; this is the first non-brute-force algorithm for solving these games. From the strategy improvement algorithm we obtain a randomized subexponential-time algorithm to solve such games."}],"publist_id":"184","doi":"10.1007/11672142_42","volume":3884,"publication_status":"published","date_created":"2018-12-11T12:09:22Z","citation":{"short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games</i>. Vol. 3884, Springer, 2006, pp. 512–23, doi:<a href=\"https://doi.org/10.1007/11672142_42\">10.1007/11672142_42</a>.","ista":"Chatterjee K, Henzinger TA. 2006. Strategy improvement and randomized subexponential algorithms for stochastic parity games. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 512–523.","ieee":"K. Chatterjee and T. A. Henzinger, “Strategy improvement and randomized subexponential algorithms for stochastic parity games,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 512–523.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2006). Strategy improvement and randomized subexponential algorithms for stochastic parity games (Vol. 3884, pp. 512–523). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. <a href=\"https://doi.org/10.1007/11672142_42\">https://doi.org/10.1007/11672142_42</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23. Springer, 2006. <a href=\"https://doi.org/10.1007/11672142_42\">https://doi.org/10.1007/11672142_42</a>.","ama":"Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523. doi:<a href=\"https://doi.org/10.1007/11672142_42\">10.1007/11672142_42</a>"},"extern":1,"quality_controlled":0,"alternative_title":["LNCS"],"author":[{"full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"status":"public"},{"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","_id":"4539","date_updated":"2021-01-12T07:59:32Z","title":"Finitary winning in omega-regular games","page":"257 - 271","month":"03","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327 and the NSF ITR grant CCR-0225610.","intvolume":"      3920","year":"2006","volume":3920,"date_created":"2018-12-11T12:09:22Z","publication_status":"published","doi":"10.1007/11691372_17","citation":{"ama":"Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol 3920. Springer; 2006:257-271. doi:<a href=\"https://doi.org/10.1007/11691372_17\">10.1007/11691372_17</a>","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2006). Finitary winning in omega-regular games (Vol. 3920, pp. 257–271). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. <a href=\"https://doi.org/10.1007/11691372_17\">https://doi.org/10.1007/11691372_17</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular Games,” 3920:257–71. Springer, 2006. <a href=\"https://doi.org/10.1007/11691372_17\">https://doi.org/10.1007/11691372_17</a>.","ista":"Chatterjee K, Henzinger TA. 2006. Finitary winning in omega-regular games. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 3920, 257–271.","ieee":"K. Chatterjee and T. A. Henzinger, “Finitary winning in omega-regular games,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2006, vol. 3920, pp. 257–271.","short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Finitary Winning in Omega-Regular Games</i>. Vol. 3920, Springer, 2006, pp. 257–71, doi:<a href=\"https://doi.org/10.1007/11691372_17\">10.1007/11691372_17</a>."},"extern":1,"quality_controlled":0,"status":"public","alternative_title":["LNCS"],"author":[{"first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2006-03-15T00:00:00Z","publisher":"Springer","day":"15","publist_id":"183","abstract":[{"lang":"eng","text":"Games on graphs with ω-regular objectives provide a model for the control and synthesis of reactive systems. Every ω-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. While for one-shot liveness (reachability) objectives, classical and finitary liveness coincide, for repeated liveness (Büchi) objectives, the finitary formulation is strictly stronger. In this work we study games with finitary parity and Streett (fairness) objectives. We prove the determinacy of these games, present algorithms for solving these games, and characterize the memory requirements of winning strategies. Our algorithms can be used, for example, for synthesizing controllers that do not let the response time of a system increase without bound."}]},{"title":"Compositional quantitative reasoning","_id":"4549","type":"conference","date_updated":"2021-01-12T07:59:37Z","conference":{"name":"QEST: Quantitative Evaluation of Systems"},"acknowledgement":"Supported in part by the NSF grants CCR-0234690, CCR-0208875, and CCR-0225610; by the NSF grant CCR-0132780 and ARP grant SC20051123.","year":"2006","month":"09","page":"179 - 188","extern":1,"citation":{"short":"K. Chatterjee, L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:, IEEE, 2006, pp. 179–188.","mla":"Chatterjee, Krishnendu, et al. <i>Compositional Quantitative Reasoning</i>. IEEE, 2006, pp. 179–88, doi:<a href=\"https://doi.org/10.1109/QEST.2006.11\">10.1109/QEST.2006.11</a>.","ista":"Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2006. Compositional quantitative reasoning. QEST: Quantitative Evaluation of Systems, 179–188.","ieee":"K. Chatterjee, L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “Compositional quantitative reasoning,” presented at the QEST: Quantitative Evaluation of Systems, 2006, pp. 179–188.","apa":"Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga, M. (2006). Compositional quantitative reasoning (pp. 179–188). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. <a href=\"https://doi.org/10.1109/QEST.2006.11\">https://doi.org/10.1109/QEST.2006.11</a>","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and Mariëlle Stoelinga. “Compositional Quantitative Reasoning,” 179–88. IEEE, 2006. <a href=\"https://doi.org/10.1109/QEST.2006.11\">https://doi.org/10.1109/QEST.2006.11</a>.","ama":"Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Compositional quantitative reasoning. In: IEEE; 2006:179-188. doi:<a href=\"https://doi.org/10.1109/QEST.2006.11\">10.1109/QEST.2006.11</a>"},"author":[{"first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"de Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"full_name":"Faella, Marco","first_name":"Marco","last_name":"Faella"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar S","last_name":"Majumdar"},{"last_name":"Stoelinga","first_name":"Mariëlle","full_name":"Stoelinga, Mariëlle"}],"quality_controlled":0,"status":"public","doi":"10.1109/QEST.2006.11","publication_status":"published","date_created":"2018-12-11T12:09:26Z","abstract":[{"text":"We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system properties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports the composition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbered distances between descriptions of a system at different levels of detail. We show that the classical Boolean rules for compositional reasoning have quantitative counterparts in our setting. While our general theory allows costs to be specified by arbitrary cost functions, we also consider a class of linear cost functions, which give rise to an instance of our framework where all operations are computable in polynomial time.","lang":"eng"}],"publist_id":"163","day":"01","publisher":"IEEE","date_published":"2006-09-01T00:00:00Z"},{"abstract":[{"text":"In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it sometimes suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of ω-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.","lang":"eng"}],"publist_id":"164","day":"07","publisher":"Elsevier","publication":"Theoretical Computer Science","date_published":"2006-08-07T00:00:00Z","citation":{"ama":"Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. <i>Theoretical Computer Science</i>. 2006;365(1-2):67-82. doi:<a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">10.1016/j.tcs.2006.07.032</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games with Secure Equilibria.” <i>Theoretical Computer Science</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">https://doi.org/10.1016/j.tcs.2006.07.032</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Jurdziński, M. (2006). Games with secure equilibria. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">https://doi.org/10.1016/j.tcs.2006.07.032</a>","ieee":"K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,” <i>Theoretical Computer Science</i>, vol. 365, no. 1–2. Elsevier, pp. 67–82, 2006.","ista":"Chatterjee K, Henzinger TA, Jurdziński M. 2006. Games with secure equilibria. Theoretical Computer Science. 365(1–2), 67–82.","short":"K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science 365 (2006) 67–82.","mla":"Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” <i>Theoretical Computer Science</i>, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:<a href=\"https://doi.org/10.1016/j.tcs.2006.07.032\">10.1016/j.tcs.2006.07.032</a>."},"extern":1,"status":"public","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"first_name":"Marcin","full_name":"Jurdziński, Marcin","last_name":"Jurdziński"}],"quality_controlled":0,"doi":"10.1016/j.tcs.2006.07.032","volume":365,"date_created":"2018-12-11T12:09:26Z","publication_status":"published","year":"2006","intvolume":"       365","month":"08","page":"67 - 82","issue":"1-2","title":"Games with secure equilibria","_id":"4550","type":"journal_article","date_updated":"2021-01-12T07:59:38Z"},{"abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple discounted reward objectives. Such MDPs occur in design problems where one wishes to simultaneously optimize several criteria, for example, latency and power. The possible trade-offs between the different objectives are characterized by the Pareto curve. We show that every Pareto-optimal point can be achieved by a memoryless strategy; however, unlike in the single-objective case, the memoryless strategy may require randomization. Moreover, we show that the Pareto curve can be approximated in polynomial time in the size of the MDP. Additionally, we study the problem if a given value vector is realizable by any strategy, and show that it can be decided in polynomial time; but the question whether it is realizable by a deterministic memoryless strategy is NP-complete. These results provide efficient algorithms for design exploration in MDP models with multiple objectives.\nThis research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202. ","lang":"eng"}],"publist_id":"161","day":"14","publisher":"Springer","date_published":"2006-02-14T00:00:00Z","extern":1,"citation":{"chicago":"Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. <a href=\"https://doi.org/10.1007/11672142_26\">https://doi.org/10.1007/11672142_26</a>.","apa":"Chatterjee, K., Majumdar, R., &#38; Henzinger, T. A. (2006). Markov decision processes with multiple objectives (Vol. 3884, pp. 325–336). Presented at the STACS: Theoretical Aspects of Computer Science, Springer. <a href=\"https://doi.org/10.1007/11672142_26\">https://doi.org/10.1007/11672142_26</a>","ama":"Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple objectives. In: Vol 3884. Springer; 2006:325-336. doi:<a href=\"https://doi.org/10.1007/11672142_26\">10.1007/11672142_26</a>","short":"K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.","mla":"Chatterjee, Krishnendu, et al. <i>Markov Decision Processes with Multiple Objectives</i>. Vol. 3884, Springer, 2006, pp. 325–36, doi:<a href=\"https://doi.org/10.1007/11672142_26\">10.1007/11672142_26</a>.","ieee":"K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Markov decision processes with multiple objectives,” presented at the STACS: Theoretical Aspects of Computer Science, 2006, vol. 3884, pp. 325–336.","ista":"Chatterjee K, Majumdar R, Henzinger TA. 2006. Markov decision processes with multiple objectives. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 3884, 325–336."},"alternative_title":["LNCS"],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar S","first_name":"Ritankar"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A"}],"status":"public","quality_controlled":0,"doi":"10.1007/11672142_26","volume":3884,"publication_status":"published","date_created":"2018-12-11T12:09:26Z","intvolume":"      3884","year":"2006","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202.","month":"02","page":"325 - 336","title":"Markov decision processes with multiple objectives","type":"conference","_id":"4551","date_updated":"2021-01-12T07:59:38Z","conference":{"name":"STACS: Theoretical Aspects of Computer Science"}},{"date_created":"2018-12-11T12:09:26Z","publication_status":"published","doi":"10.1109/QEST.2006.48","citation":{"ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent reachability games. QEST: Quantitative Evaluation of Systems, 291–300.","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for concurrent reachability games,” presented at the QEST: Quantitative Evaluation of Systems, 2006, pp. 291–300.","mla":"Chatterjee, Krishnendu, et al. <i>Strategy Improvement for Concurrent Reachability Games</i>. IEEE, 2006, pp. 291–300, doi:<a href=\"https://doi.org/10.1109/QEST.2006.48\">10.1109/QEST.2006.48</a>.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300.","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent reachability games. In: IEEE; 2006:291-300. doi:<a href=\"https://doi.org/10.1109/QEST.2006.48\">10.1109/QEST.2006.48</a>","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2006). Strategy improvement for concurrent reachability games (pp. 291–300). Presented at the QEST: Quantitative Evaluation of Systems, IEEE. <a href=\"https://doi.org/10.1109/QEST.2006.48\">https://doi.org/10.1109/QEST.2006.48</a>","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy Improvement for Concurrent Reachability Games,” 291–300. IEEE, 2006. <a href=\"https://doi.org/10.1109/QEST.2006.48\">https://doi.org/10.1109/QEST.2006.48</a>."},"extern":1,"status":"public","quality_controlled":0,"author":[{"first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"de Alfaro, Luca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"date_published":"2006-01-01T00:00:00Z","publisher":"IEEE","day":"01","publist_id":"162","abstract":[{"text":"A concurrent reachability game is a two-player game played on a graph: at each state, the players simultaneously and independently select moves; the two moves determine jointly a probability distribution over the successor states. The objective for player 1 consists in reaching a set of target states; the objective for player 2 is to prevent this, so that the game is zero-sum. Our contributions are two-fold. First, we present a simple proof of the fact that in concurrent reachability games, for all epsilon &gt; 0, memoryless epsilon-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal strategy achieves the objective with probability within epsilon of the value of the game. In contrast to previous proofs of this fact, which rely on the limit behavior of discounted games using advanced Puisieux series analysis, our proof is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives.","lang":"eng"}],"conference":{"name":"QEST: Quantitative Evaluation of Systems"},"type":"conference","_id":"4552","date_updated":"2021-01-12T07:59:39Z","title":"Strategy improvement for concurrent reachability games","page":"291 - 300","month":"01","year":"2006"},{"conference":{"name":"CAV: Computer Aided Verification"},"date_updated":"2021-01-12T07:59:49Z","_id":"4574","type":"conference","title":"Lazy shape analysis","page":"532 - 546","month":"08","year":"2006","intvolume":"      4144","date_created":"2018-12-11T12:09:33Z","publication_status":"published","volume":4144,"doi":"10.1007/11817963_48","quality_controlled":0,"status":"public","author":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"Dirk"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Grégory","full_name":"Théoduloz, Grégory","last_name":"Théoduloz"}],"alternative_title":["LNCS"],"extern":1,"citation":{"ieee":"D. Beyer, T. A. Henzinger, and G. Théoduloz, “Lazy shape analysis,” presented at the CAV: Computer Aided Verification, 2006, vol. 4144, pp. 532–546.","ista":"Beyer D, Henzinger TA, Théoduloz G. 2006. Lazy shape analysis. CAV: Computer Aided Verification, LNCS, vol. 4144, 532–546.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2006, pp. 532–546.","mla":"Beyer, Dirk, et al. <i>Lazy Shape Analysis</i>. Vol. 4144, Springer, 2006, pp. 532–46, doi:<a href=\"https://doi.org/10.1007/11817963_48\">10.1007/11817963_48</a>.","ama":"Beyer D, Henzinger TA, Théoduloz G. Lazy shape analysis. In: Vol 4144. Springer; 2006:532-546. doi:<a href=\"https://doi.org/10.1007/11817963_48\">10.1007/11817963_48</a>","apa":"Beyer, D., Henzinger, T. A., &#38; Théoduloz, G. (2006). Lazy shape analysis (Vol. 4144, pp. 532–546). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/11817963_48\">https://doi.org/10.1007/11817963_48</a>","chicago":"Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Lazy Shape Analysis,” 4144:532–46. Springer, 2006. <a href=\"https://doi.org/10.1007/11817963_48\">https://doi.org/10.1007/11817963_48</a>."},"date_published":"2006-08-08T00:00:00Z","publisher":"Springer","day":"08","publist_id":"133","abstract":[{"lang":"eng","text":"Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker Blast. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending Blast with calls to Tvla."}]},{"issue":"175","page":"573-587","month":"10","intvolume":"        51","type":"journal_article","main_file_link":[{"url":"https://doi.org/10.3189/172756505781829124","open_access":"1"}],"publication":"Journal of Glaciology","scopus_import":"1","publisher":"Cambridge University Press","language":[{"iso":"eng"}],"abstract":[{"text":"An enhanced temperature-index glacier melt model, incorporating incoming shortwave radiation and albedo, is presented. The model is an attempt to combine the high temporal resolution and accuracy of physically based melt models with the lower data requirements and computational simplicity of empirical melt models, represented by the ‘degree-day’ method and its variants. The model is run with both measured and modelled radiation data, to test its applicability to glaciers with differing data availability. Five automatic weather stations were established on Haut Glacier d’Arolla, Switzerland, between May and September 2001. Reference surface melt rates were calculated using a physically based energy-balance melt model. The performance of the enhanced temperature-index model was tested at each of the four validation stations by comparing predicted hourly melt rates with reference melt rates. Predictions made with three other temperature-index models were evaluated in the same way for comparison. The enhanced temperature-index model offers significant improvements over the other temperature-index models, and accounts for 90–95% of the variation in the reference melt rate. The improvement is lower, but still significant, when the model is forced by modelled shortwave radiation data, thus offering a better alternative to existing models that require only temperature data input.","lang":"eng"}],"publication_status":"published","article_type":"original","quality_controlled":"1","citation":{"short":"F. Pellicciotti, B. Brock, U. Strasser, P. Burlando, M. Funk, J. Corripio, Journal of Glaciology 51 (2005) 573–587.","mla":"Pellicciotti, Francesca, et al. “An Enhanced Temperature-Index Glacier Melt Model Including the Shortwave Radiation Balance: Development and Testing for Haut Glacier d’Arolla, Switzerland.” <i>Journal of Glaciology</i>, vol. 51, no. 175, Cambridge University Press, 2005, pp. 573–87, doi:<a href=\"https://doi.org/10.3189/172756505781829124\">10.3189/172756505781829124</a>.","ieee":"F. Pellicciotti, B. Brock, U. Strasser, P. Burlando, M. Funk, and J. Corripio, “An enhanced temperature-index glacier melt model including the shortwave radiation balance: Development and testing for Haut Glacier d’Arolla, Switzerland,” <i>Journal of Glaciology</i>, vol. 51, no. 175. Cambridge University Press, pp. 573–587, 2005.","ista":"Pellicciotti F, Brock B, Strasser U, Burlando P, Funk M, Corripio J. 2005. An enhanced temperature-index glacier melt model including the shortwave radiation balance: Development and testing for Haut Glacier d’Arolla, Switzerland. Journal of Glaciology. 51(175), 573–587.","chicago":"Pellicciotti, Francesca, Ben Brock, Ulrich Strasser, Paolo Burlando, Martin Funk, and Javier Corripio. “An Enhanced Temperature-Index Glacier Melt Model Including the Shortwave Radiation Balance: Development and Testing for Haut Glacier d’Arolla, Switzerland.” <i>Journal of Glaciology</i>. Cambridge University Press, 2005. <a href=\"https://doi.org/10.3189/172756505781829124\">https://doi.org/10.3189/172756505781829124</a>.","apa":"Pellicciotti, F., Brock, B., Strasser, U., Burlando, P., Funk, M., &#38; Corripio, J. (2005). An enhanced temperature-index glacier melt model including the shortwave radiation balance: Development and testing for Haut Glacier d’Arolla, Switzerland. <i>Journal of Glaciology</i>. Cambridge University Press. <a href=\"https://doi.org/10.3189/172756505781829124\">https://doi.org/10.3189/172756505781829124</a>","ama":"Pellicciotti F, Brock B, Strasser U, Burlando P, Funk M, Corripio J. An enhanced temperature-index glacier melt model including the shortwave radiation balance: Development and testing for Haut Glacier d’Arolla, Switzerland. <i>Journal of Glaciology</i>. 2005;51(175):573-587. doi:<a href=\"https://doi.org/10.3189/172756505781829124\">10.3189/172756505781829124</a>"},"publication_identifier":{"eissn":["1727-5652"],"issn":["0022-1430"]},"oa":1,"year":"2005","date_updated":"2023-02-20T08:45:37Z","_id":"12657","title":"An enhanced temperature-index glacier melt model including the shortwave radiation balance: Development and testing for Haut Glacier d’Arolla, Switzerland","article_processing_charge":"No","date_published":"2005-10-19T00:00:00Z","day":"19","date_created":"2023-02-20T08:18:51Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":51,"doi":"10.3189/172756505781829124","author":[{"id":"b28f055a-81ea-11ed-b70c-a9fe7f7b0e70","last_name":"Pellicciotti","first_name":"Francesca","full_name":"Pellicciotti, Francesca"},{"last_name":"Brock","full_name":"Brock, Ben","first_name":"Ben"},{"last_name":"Strasser","first_name":"Ulrich","full_name":"Strasser, Ulrich"},{"last_name":"Burlando","first_name":"Paolo","full_name":"Burlando, Paolo"},{"first_name":"Martin","full_name":"Funk, Martin","last_name":"Funk"},{"full_name":"Corripio, Javier","first_name":"Javier","last_name":"Corripio"}],"status":"public","extern":"1","oa_version":"Published Version"},{"publisher":"Society for Neuroscience","day":"11","publication":"Journal of Neuroscience","date_published":"2005-03-11T00:00:00Z","abstract":[{"lang":"eng","text":"Genetically encoded fluorescent probes of neural activity represent new promising tools for systems neuroscience. Here, we present a comparative in vivo analysis of 10 different genetically encoded calcium indicators, as well as the pH-sensitive synapto-pHluorin. We analyzed their fluorescence changes in presynaptic boutons of the Drosophila larval neuromuscular junction. Robust neural activity did not result in any or noteworthy fluorescence changes when Flash-Pericam, Camgaroo-1, and Camgaroo-2 were expressed. However, calculated on the raw data, fractional fluorescence changes up to 18% were reported by synapto-pHluorin, Yellow Cameleon 2.0, 2.3, and 3.3, Inverse-Pericam, GCaMP1.3, GCaMP1.6, and the troponin C-based calcium sensor TN-L15. The response characteristics of all of these indicators differed considerably from each other, with GCaMP1.6 reporting high rates of neural activity with the largest and fastest fluorescence changes. However, GCaMP1.6 suffered from photobleaching, whereas the fluorescence signals of the double-chromophore indicators were in general smaller but more photostable and reproducible, with TN-L15 showing the fastest rise of the signals at lower activity rates. We show for GCaMP1.3 and YC3.3 that an expanded range of neural activity evoked fairly linear fluorescence changes and a corresponding linear increase in the signal-to-noise ratio (SNR). The expression level of the indicator biased the signal kinetics and SNR, whereas the signal amplitude was independent. The presented data will be useful for in vivo experiments with respect to the selection of an appropriate indicator, as well as for the correct interpretation of the optical signals."}],"publist_id":"5975","doi":"10.1523/JNEUROSCI.4900-04.2005","volume":25,"date_created":"2018-12-11T11:51:13Z","publication_status":"published","citation":{"short":"D. Reiff, A. Ihring, G. Guerrero, E. Isacoff, M.A. Jösch, J. Nakai, A. Borst, Journal of Neuroscience 25 (2005) 4766–4778.","mla":"Reiff, Dierk, et al. “In Vivo Performance of Genetically Encoded Indicators of Neural Activity in Flies.” <i>Journal of Neuroscience</i>, vol. 25, no. 19, Society for Neuroscience, 2005, pp. 4766–78, doi:<a href=\"https://doi.org/10.1523/JNEUROSCI.4900-04.2005\">10.1523/JNEUROSCI.4900-04.2005</a>.","ista":"Reiff D, Ihring A, Guerrero G, Isacoff E, Jösch MA, Nakai J, Borst A. 2005. In vivo performance of genetically encoded indicators of neural activity in flies. Journal of Neuroscience. 25(19), 4766–4778.","ieee":"D. Reiff <i>et al.</i>, “In vivo performance of genetically encoded indicators of neural activity in flies,” <i>Journal of Neuroscience</i>, vol. 25, no. 19. Society for Neuroscience, pp. 4766–4778, 2005.","apa":"Reiff, D., Ihring, A., Guerrero, G., Isacoff, E., Jösch, M. A., Nakai, J., &#38; Borst, A. (2005). In vivo performance of genetically encoded indicators of neural activity in flies. <i>Journal of Neuroscience</i>. Society for Neuroscience. <a href=\"https://doi.org/10.1523/JNEUROSCI.4900-04.2005\">https://doi.org/10.1523/JNEUROSCI.4900-04.2005</a>","chicago":"Reiff, Dierk, Alexandra Ihring, Giovanna Guerrero, Ehud Isacoff, Maximilian A Jösch, Junichi Nakai, and Alexander Borst. “In Vivo Performance of Genetically Encoded Indicators of Neural Activity in Flies.” <i>Journal of Neuroscience</i>. Society for Neuroscience, 2005. <a href=\"https://doi.org/10.1523/JNEUROSCI.4900-04.2005\">https://doi.org/10.1523/JNEUROSCI.4900-04.2005</a>.","ama":"Reiff D, Ihring A, Guerrero G, et al. In vivo performance of genetically encoded indicators of neural activity in flies. <i>Journal of Neuroscience</i>. 2005;25(19):4766-4778. doi:<a href=\"https://doi.org/10.1523/JNEUROSCI.4900-04.2005\">10.1523/JNEUROSCI.4900-04.2005</a>"},"extern":1,"status":"public","quality_controlled":0,"author":[{"first_name":"Dierk","full_name":"Reiff, Dierk F","last_name":"Reiff"},{"last_name":"Ihring","full_name":"Ihring, Alexandra","first_name":"Alexandra"},{"last_name":"Guerrero","first_name":"Giovanna","full_name":"Guerrero, Giovanna"},{"full_name":"Isacoff, Ehud Y","first_name":"Ehud","last_name":"Isacoff"},{"orcid":"0000-0002-3937-1330","first_name":"Maximilian A","full_name":"Maximilian Jösch","last_name":"Jösch","id":"2BD278E6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Junichi","full_name":"Nakai, Junichi","last_name":"Nakai"},{"last_name":"Borst","full_name":"Borst, Alexander","first_name":"Alexander"}],"page":"4766 - 4778","issue":"19","intvolume":"        25","acknowledgement":"This work was supported by the Max-Planck-Society.","year":"2005","month":"03","_id":"1298","type":"journal_article","date_updated":"2021-01-12T06:49:42Z","title":"In vivo performance of genetically encoded indicators of neural activity in flies"},{"doi":"10.1093/hmg/ddi350","date_created":"2018-12-11T11:48:48Z","publication_status":"published","volume":14,"quality_controlled":0,"author":[{"first_name":"Lev","full_name":"Yampolsky, Lev Y","last_name":"Yampolsky"},{"last_name":"Kondrashov","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8243-4694","full_name":"Fyodor Kondrashov","first_name":"Fyodor"},{"last_name":"Kondrashov","full_name":"Kondrashov, Alexey S","first_name":"Alexey"}],"status":"public","citation":{"apa":"Yampolsky, L., Kondrashov, F., &#38; Kondrashov, A. (2005). Distribution of the strength of selection against amino acid replacements in human proteins. <i>Human Molecular Genetics</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/hmg/ddi350\">https://doi.org/10.1093/hmg/ddi350</a>","chicago":"Yampolsky, Lev, Fyodor Kondrashov, and Alexey Kondrashov. “Distribution of the Strength of Selection against Amino Acid Replacements in Human Proteins.” <i>Human Molecular Genetics</i>. Oxford University Press, 2005. <a href=\"https://doi.org/10.1093/hmg/ddi350\">https://doi.org/10.1093/hmg/ddi350</a>.","ama":"Yampolsky L, Kondrashov F, Kondrashov A. Distribution of the strength of selection against amino acid replacements in human proteins. <i>Human Molecular Genetics</i>. 2005;14(21):3191-3201. doi:<a href=\"https://doi.org/10.1093/hmg/ddi350\">10.1093/hmg/ddi350</a>","mla":"Yampolsky, Lev, et al. “Distribution of the Strength of Selection against Amino Acid Replacements in Human Proteins.” <i>Human Molecular Genetics</i>, vol. 14, no. 21, Oxford University Press, 2005, pp. 3191–201, doi:<a href=\"https://doi.org/10.1093/hmg/ddi350\">10.1093/hmg/ddi350</a>.","short":"L. Yampolsky, F. Kondrashov, A. Kondrashov, Human Molecular Genetics 14 (2005) 3191–3201.","ieee":"L. Yampolsky, F. Kondrashov, and A. Kondrashov, “Distribution of the strength of selection against amino acid replacements in human proteins,” <i>Human Molecular Genetics</i>, vol. 14, no. 21. Oxford University Press, pp. 3191–3201, 2005.","ista":"Yampolsky L, Kondrashov F, Kondrashov A. 2005. Distribution of the strength of selection against amino acid replacements in human proteins. Human Molecular Genetics. 14(21), 3191–3201."},"extern":1,"publisher":"Oxford University Press","day":"01","date_published":"2005-11-01T00:00:00Z","publication":"Human Molecular Genetics","abstract":[{"text":"The impact of an amino acid replacement on the organism's fitness can vary from lethal to selectively neutral and even, in rare cases, beneficial. Substantial data are available on either pathogenic or acceptable replacements. However, the whole distribution of coefficients of selection against individual replacements is not known for any organism. To ascertain this distribution for human proteins, we combined data on pathogenic missense mutations, on human non-synonymous SNPs and on human-chimpanzee divergence of orthologous proteins. Fractions of amino acid replacements which reduce fitness by &gt;10-2, 10-2-10-4, 10-4-10-5 and &lt;10-5 are 25, 49, 14 and 12%, respectively. On average, the strength of selection against a replacement is substantially higher when chemically dissimilar amino acids are involved, and the Grantham's index of a replacement explains 35% of variance in the average logarithm of selection coefficients associated with different replacements. Still, the impact of a replacement depends on its context within the protein more than on its own nature. Reciprocal replacements are often associated with rather different selection coefficients, in particular, replacements of non-polar amino acids with polar ones are typically much more deleterious than replacements in the opposite direction. However, differences between evolutionary fluxes of reciprocal replacements are only weakly correlated with the differences between the corresponding selection coefficients.","lang":"eng"}],"publist_id":"6807","date_updated":"2021-01-12T08:19:13Z","type":"journal_article","_id":"843","title":"Distribution of the strength of selection against amino acid replacements in human proteins","page":"3191 - 3201","issue":"21","year":"2005","intvolume":"        14","month":"11"},{"abstract":[{"lang":"eng","text":"Fast multidimensional NMR with a time resolution of a few seconds provides a new tool for high throughput screening and site-resolved real-time studies of kinetic molecular processes by NMR. Recently we have demonstrated the feasibility to record protein 1H–15N correlation spectra in a few seconds of acquisition time using a new SOFAST-HMQC experiment (Schanda and Brutscher (2005) J. Am. Chem. Soc. 127, 8014). Here, we investigate in detail the performance of SOFAST-HMQC to record 1H–15N and 1H−13C correlation spectra of proteins of different size and at different magnetic field strengths. Compared to standard 1H–15N correlation experiments SOFAST-HMQC provides a significant gain in sensitivity, especially for fast repetition rates. Guidelines are provided on how to set up SOFAST-HMQC experiments for a given protein sample. In addition, an alternative pulse scheme, IPAP-SOFAST-HMQC is presented that allows application on NMR spectrometers equipped with cryogenic probes, and fast measurement of one-bond 1H–13C and 1H–15N scalar and residual dipolar coupling constants."}],"language":[{"iso":"eng"}],"day":"01","publisher":"Springer Nature","date_published":"2005-12-01T00:00:00Z","publication":"Journal of Biomolecular NMR","oa_version":"None","author":[{"full_name":"Schanda, Paul","first_name":"Paul","orcid":"0000-0002-9350-7606","id":"7B541462-FAF6-11E9-A490-E8DFE5697425","last_name":"Schanda"},{"last_name":"Kupče","first_name":"Ēriks","full_name":"Kupče, Ēriks"},{"first_name":"Bernhard","full_name":"Brutscher, Bernhard","last_name":"Brutscher"}],"quality_controlled":"1","status":"public","keyword":["Spectroscopy","Biochemistry"],"citation":{"ama":"Schanda P, Kupče Ē, Brutscher B. SOFAST-HMQC experiments for recording two-dimensional deteronuclear correlation spectra of proteins within a few seconds. <i>Journal of Biomolecular NMR</i>. 2005;33(4):199-211. doi:<a href=\"https://doi.org/10.1007/s10858-005-4425-x\">10.1007/s10858-005-4425-x</a>","apa":"Schanda, P., Kupče, Ē., &#38; Brutscher, B. (2005). SOFAST-HMQC experiments for recording two-dimensional deteronuclear correlation spectra of proteins within a few seconds. <i>Journal of Biomolecular NMR</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10858-005-4425-x\">https://doi.org/10.1007/s10858-005-4425-x</a>","chicago":"Schanda, Paul, Ēriks Kupče, and Bernhard Brutscher. “SOFAST-HMQC Experiments for Recording Two-Dimensional Deteronuclear Correlation Spectra of Proteins within a Few Seconds.” <i>Journal of Biomolecular NMR</i>. Springer Nature, 2005. <a href=\"https://doi.org/10.1007/s10858-005-4425-x\">https://doi.org/10.1007/s10858-005-4425-x</a>.","ieee":"P. Schanda, Ē. Kupče, and B. Brutscher, “SOFAST-HMQC experiments for recording two-dimensional deteronuclear correlation spectra of proteins within a few seconds,” <i>Journal of Biomolecular NMR</i>, vol. 33, no. 4. Springer Nature, pp. 199–211, 2005.","ista":"Schanda P, Kupče Ē, Brutscher B. 2005. SOFAST-HMQC experiments for recording two-dimensional deteronuclear correlation spectra of proteins within a few seconds. Journal of Biomolecular NMR. 33(4), 199–211.","mla":"Schanda, Paul, et al. “SOFAST-HMQC Experiments for Recording Two-Dimensional Deteronuclear Correlation Spectra of Proteins within a Few Seconds.” <i>Journal of Biomolecular NMR</i>, vol. 33, no. 4, Springer Nature, 2005, pp. 199–211, doi:<a href=\"https://doi.org/10.1007/s10858-005-4425-x\">10.1007/s10858-005-4425-x</a>.","short":"P. Schanda, Ē. Kupče, B. Brutscher, Journal of Biomolecular NMR 33 (2005) 199–211."},"extern":"1","doi":"10.1007/s10858-005-4425-x","article_type":"original","date_created":"2020-09-18T10:13:59Z","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":33,"year":"2005","intvolume":"        33","month":"12","page":"199-211","publication_identifier":{"issn":["0925-2738","1573-5001"]},"issue":"4","article_processing_charge":"No","title":"SOFAST-HMQC experiments for recording two-dimensional deteronuclear correlation spectra of proteins within a few seconds","date_updated":"2021-01-12T08:19:38Z","type":"journal_article","_id":"8491"},{"month":"05","intvolume":"       127","year":"2005","issue":"22","publication_identifier":{"issn":["0002-7863","1520-5126"]},"page":"8014-8015","title":"Very fast two-dimensional NMR spectroscopy for real-time investigation of dynamic events in proteins on the time scale of seconds","article_processing_charge":"No","type":"journal_article","_id":"8492","date_updated":"2021-01-12T08:19:39Z","language":[{"iso":"eng"}],"abstract":[{"text":"We demonstrate for different protein samples that 2D 1H−15N correlation NMR spectra can be recorded in a few seconds of acquisition time using a new band-selective optimized flip-angle short-transient heteronuclear multiple quantum coherence experiment. This has enabled us to measure fast hydrogen−deuterium exchange rate constants along the backbone of a small globular protein fragment by real-time 2D NMR.","lang":"eng"}],"publication":"Journal of the American Chemical Society","date_published":"2005-05-14T00:00:00Z","publisher":"American Chemical Society","day":"14","keyword":["Colloid and Surface Chemistry","Biochemistry","General Chemistry","Catalysis"],"citation":{"chicago":"Schanda, Paul, and Bernhard Brutscher. “Very Fast Two-Dimensional NMR Spectroscopy for Real-Time Investigation of Dynamic Events in Proteins on the Time Scale of Seconds.” <i>Journal of the American Chemical Society</i>. American Chemical Society, 2005. <a href=\"https://doi.org/10.1021/ja051306e\">https://doi.org/10.1021/ja051306e</a>.","apa":"Schanda, P., &#38; Brutscher, B. (2005). Very fast two-dimensional NMR spectroscopy for real-time investigation of dynamic events in proteins on the time scale of seconds. <i>Journal of the American Chemical Society</i>. American Chemical Society. <a href=\"https://doi.org/10.1021/ja051306e\">https://doi.org/10.1021/ja051306e</a>","ama":"Schanda P, Brutscher B. Very fast two-dimensional NMR spectroscopy for real-time investigation of dynamic events in proteins on the time scale of seconds. <i>Journal of the American Chemical Society</i>. 2005;127(22):8014-8015. doi:<a href=\"https://doi.org/10.1021/ja051306e\">10.1021/ja051306e</a>","mla":"Schanda, Paul, and Bernhard Brutscher. “Very Fast Two-Dimensional NMR Spectroscopy for Real-Time Investigation of Dynamic Events in Proteins on the Time Scale of Seconds.” <i>Journal of the American Chemical Society</i>, vol. 127, no. 22, American Chemical Society, 2005, pp. 8014–15, doi:<a href=\"https://doi.org/10.1021/ja051306e\">10.1021/ja051306e</a>.","short":"P. Schanda, B. Brutscher, Journal of the American Chemical Society 127 (2005) 8014–8015.","ieee":"P. Schanda and B. Brutscher, “Very fast two-dimensional NMR spectroscopy for real-time investigation of dynamic events in proteins on the time scale of seconds,” <i>Journal of the American Chemical Society</i>, vol. 127, no. 22. American Chemical Society, pp. 8014–8015, 2005.","ista":"Schanda P, Brutscher B. 2005. Very fast two-dimensional NMR spectroscopy for real-time investigation of dynamic events in proteins on the time scale of seconds. Journal of the American Chemical Society. 127(22), 8014–8015."},"extern":"1","author":[{"orcid":"0000-0002-9350-7606","first_name":"Paul","full_name":"Schanda, Paul","last_name":"Schanda","id":"7B541462-FAF6-11E9-A490-E8DFE5697425"},{"full_name":"Brutscher, Bernhard","first_name":"Bernhard","last_name":"Brutscher"}],"quality_controlled":"1","status":"public","oa_version":"None","volume":127,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2020-09-18T10:14:05Z","publication_status":"published","doi":"10.1021/ja051306e","article_type":"original"},{"article_processing_charge":"No","title":"On diffusion in high-dimensional Hamiltonian systems","date_updated":"2021-01-12T08:19:49Z","type":"journal_article","_id":"8516","month":"12","intvolume":"       229","year":"2005","publication_identifier":{"issn":["0022-1236"]},"issue":"1","page":"1-61","author":[{"last_name":"Bourgain","full_name":"Bourgain, Jean","first_name":"Jean"},{"id":"FE553552-CDE8-11E9-B324-C0EBE5697425","last_name":"Kaloshin","full_name":"Kaloshin, Vadim","first_name":"Vadim","orcid":"0000-0002-6051-2628"}],"quality_controlled":"1","status":"public","citation":{"ieee":"J. Bourgain and V. Kaloshin, “On diffusion in high-dimensional Hamiltonian systems,” <i>Journal of Functional Analysis</i>, vol. 229, no. 1. Elsevier, pp. 1–61, 2005.","ista":"Bourgain J, Kaloshin V. 2005. On diffusion in high-dimensional Hamiltonian systems. Journal of Functional Analysis. 229(1), 1–61.","mla":"Bourgain, Jean, and Vadim Kaloshin. “On Diffusion in High-Dimensional Hamiltonian Systems.” <i>Journal of Functional Analysis</i>, vol. 229, no. 1, Elsevier, 2005, pp. 1–61, doi:<a href=\"https://doi.org/10.1016/j.jfa.2004.09.006\">10.1016/j.jfa.2004.09.006</a>.","short":"J. Bourgain, V. Kaloshin, Journal of Functional Analysis 229 (2005) 1–61.","ama":"Bourgain J, Kaloshin V. On diffusion in high-dimensional Hamiltonian systems. <i>Journal of Functional Analysis</i>. 2005;229(1):1-61. doi:<a href=\"https://doi.org/10.1016/j.jfa.2004.09.006\">10.1016/j.jfa.2004.09.006</a>","chicago":"Bourgain, Jean, and Vadim Kaloshin. “On Diffusion in High-Dimensional Hamiltonian Systems.” <i>Journal of Functional Analysis</i>. Elsevier, 2005. <a href=\"https://doi.org/10.1016/j.jfa.2004.09.006\">https://doi.org/10.1016/j.jfa.2004.09.006</a>.","apa":"Bourgain, J., &#38; Kaloshin, V. (2005). On diffusion in high-dimensional Hamiltonian systems. <i>Journal of Functional Analysis</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jfa.2004.09.006\">https://doi.org/10.1016/j.jfa.2004.09.006</a>"},"keyword":["Analysis"],"extern":"1","oa_version":"None","publication_status":"published","date_created":"2020-09-18T10:49:06Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":229,"article_type":"original","doi":"10.1016/j.jfa.2004.09.006","language":[{"iso":"eng"}],"abstract":[{"text":"The purpose of this paper is to construct examples of diffusion for E-Hamiltonian perturbations\r\nof completely integrable Hamiltonian systems in 2d-dimensional phase space, with d large.\r\nIn the first part of the paper, simple and explicit examples are constructed illustrating absence\r\nof ‘long-time’ stability for size E Hamiltonian perturbations of quasi-convex integrable systems\r\nalready when the dimension 2d of phase space becomes as large as log 1/E . We first produce\r\nthe example in Gevrey class and then a real analytic one, with some additional work.\r\nIn the second part, we consider again E-Hamiltonian perturbations of completely integrable\r\nHamiltonian system in 2d-dimensional space with E-small but not too small, |E| > exp(−d), with\r\nd the number of degrees of freedom assumed large. It is shown that for a class of analytic\r\ntime-periodic perturbations, there exist linearly diffusing trajectories. The underlying idea for\r\nboth examples is similar and consists in coupling a fixed degree of freedom with a large\r\nnumber of them. The procedure and analytical details are however significantly different. As\r\nmentioned, the construction in Part I is totally elementary while Part II is more involved, relying\r\nin particular on the theory of normally hyperbolic invariant manifolds, methods of generating\r\nfunctions, Aubry–Mather theory, and Mather’s variational methods.","lang":"eng"}],"date_published":"2005-12-01T00:00:00Z","publication":"Journal of Functional Analysis","publisher":"Elsevier","day":"01"}]