---
_id: '4432'
abstract:
- lang: eng
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.
acknowledgement: This research was supported in part by the NSF grants CCR-0208875,
CCR-0225610, and CCR-0234690.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
citation:
ama: 'Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202.
Springer; 2006:1-17. doi:10.1007/11867340_1'
apa: 'Henzinger, T. A., & 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. https://doi.org/10.1007/11867340_1'
chicago: Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal
Logic,” 4202:1–17. Springer, 2006. https://doi.org/10.1007/11867340_1.
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.'
ista: 'Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.'
mla: Henzinger, Thomas A., and Vinayak Prabhu. Timed Alternating-Time Temporal
Logic. Vol. 4202, Springer, 2006, pp. 1–17, doi:10.1007/11867340_1.
short: T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:49Z
date_published: 2006-09-19T00:00:00Z
date_updated: 2021-01-12T07:56:56Z
day: '19'
doi: 10.1007/11867340_1
extern: 1
intvolume: ' 4202'
month: '09'
page: 1 - 17
publication_status: published
publisher: Springer
publist_id: '296'
quality_controlled: 0
status: public
title: Timed alternating-time temporal logic
type: conference
volume: 4202
year: '2006'
...
---
_id: '4436'
abstract:
- lang: eng
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.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Matic S. An interface algebra for real-time components. In:
IEEE; 2006:253-266. doi:10.1109/RTAS.2006.11'
apa: 'Henzinger, T. A., & 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. https://doi.org/10.1109/RTAS.2006.11'
chicago: Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time
Components,” 253–66. IEEE, 2006. https://doi.org/10.1109/RTAS.2006.11.
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.'
mla: Henzinger, Thomas A., and Slobodan Matic. An Interface Algebra for Real-Time
Components. IEEE, 2006, pp. 253–66, doi:10.1109/RTAS.2006.11.
short: T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266.
conference:
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
date_created: 2018-12-11T12:08:50Z
date_published: 2006-04-24T00:00:00Z
date_updated: 2021-01-12T07:56:57Z
day: '24'
doi: 10.1109/RTAS.2006.11
extern: 1
month: '04'
page: 253 - 266
publication_status: published
publisher: IEEE
publist_id: '294'
quality_controlled: 0
status: public
title: An interface algebra for real-time components
type: conference
year: '2006'
...
---
_id: '4437'
abstract:
- lang: eng
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.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Henzinger TA, Piterman N. Solving games without determinization. In: Vol 4207.
Springer; 2006:395-410. doi:10.1007/11874683_26'
apa: 'Henzinger, T. A., & Piterman, N. (2006). Solving games without determinization
(Vol. 4207, pp. 395–410). Presented at the CSL: Computer Science Logic, Springer.
https://doi.org/10.1007/11874683_26'
chicago: Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization,”
4207:395–410. Springer, 2006. https://doi.org/10.1007/11874683_26.
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.'
mla: Henzinger, Thomas A., and Nir Piterman. Solving Games without Determinization.
Vol. 4207, Springer, 2006, pp. 395–410, doi:10.1007/11874683_26.
short: T.A. Henzinger, N. Piterman, in:, Springer, 2006, pp. 395–410.
conference:
name: 'CSL: Computer Science Logic'
date_created: 2018-12-11T12:08:51Z
date_published: 2006-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:58Z
day: '20'
doi: 10.1007/11874683_26
extern: 1
intvolume: ' 4207'
month: '09'
page: 395 - 410
publication_status: published
publisher: Springer
publist_id: '295'
quality_controlled: 0
status: public
title: Solving games without determinization
type: conference
volume: 4207
year: '2006'
...
---
_id: '4451'
abstract:
- lang: eng
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.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
of the mu-calculus. Theoretical Computer Science. 2006;354(2):173-186.
doi:10.1016/j.tcs.2005.11.015
apa: Henzinger, T. A., Kupferman, O., & Majumdar, R. (2006). On the universal
and existential fragments of the mu-calculus. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2005.11.015
chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science.
Elsevier, 2006. https://doi.org/10.1016/j.tcs.2005.11.015.
ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
fragments of the mu-calculus,” Theoretical Computer Science, 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.
mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
the Mu-Calculus.” Theoretical Computer Science, vol. 354, no. 2, Elsevier,
2006, pp. 173–86, doi:10.1016/j.tcs.2005.11.015.
short: T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354
(2006) 173–186.
date_created: 2018-12-11T12:08:55Z
date_published: 2006-03-28T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '28'
doi: 10.1016/j.tcs.2005.11.015
extern: 1
intvolume: ' 354'
issue: '2'
month: '03'
page: 173 - 186
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '276'
quality_controlled: 0
status: public
title: On the universal and existential fragments of the mu-calculus
type: journal_article
volume: 354
year: '2006'
...
---
_id: '4523'
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.
author:
- first_name: Bhargav
full_name: Gulavani, Bhargav S
last_name: Gulavani
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Yamini
full_name: Kannan, Yamini
last_name: Kannan
- first_name: Aditya
full_name: Nori, Aditya V
last_name: Nori
- first_name: Sriram
full_name: Rajamani, Sriram K
last_name: Rajamani
citation:
ama: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm
for property checking. In: ACM; 2006:117-127. doi:10.1145/1181775.1181790'
apa: 'Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., & Rajamani, S. (2006).
Synergy: A new algorithm for property checking (pp. 117–127). Presented at the
FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1181775.1181790'
chicago: 'Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and
Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM,
2006. https://doi.org/10.1145/1181775.1181790.'
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.'
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.'
mla: 'Gulavani, Bhargav, et al. Synergy: A New Algorithm for Property Checking.
ACM, 2006, pp. 117–27, doi:10.1145/1181775.1181790.'
short: B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006,
pp. 117–127.
conference:
name: 'FSE: Foundations of Software Engineering'
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '01'
doi: 10.1145/1181775.1181790
extern: 1
month: '01'
page: 117 - 127
publication_status: published
publisher: ACM
publist_id: '206'
quality_controlled: 0
status: public
title: 'Synergy: A new algorithm for property checking'
type: conference
year: '2006'
...
---
_id: '4526'
abstract:
- lang: eng
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 "foreign" languages.
As a case study, we present a distributed HTL implementation of an automotive
steer-by-wire controller.'
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
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:10.1145/1176887.1176907'
apa: 'Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., & Sangiovanni Vincentelli,
A. (2006). A hierarchical coordination language for interacting real-time tasks
(pp. 132–141). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1176887.1176907'
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. https://doi.org/10.1145/1176887.1176907.
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. A Hierarchical Coordination Language for Interacting
Real-Time Tasks. ACM, 2006, pp. 132–41, doi:10.1145/1176887.1176907.
short: A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, A. Sangiovanni Vincentelli,
in:, ACM, 2006, pp. 132–141.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '01'
doi: 10.1145/1176887.1176907
extern: 1
month: '01'
page: 132 - 141
publication_status: published
publisher: ACM
publist_id: '201'
quality_controlled: 0
status: public
title: A hierarchical coordination language for interacting real-time tasks
type: conference
year: '2006'
...
---
_id: '4528'
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.
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Fisher J, Henzinger TA. Executable biology. In: IEEE; 2006:1675-1682. doi:10.1109/WSC.2006.322942'
apa: 'Fisher, J., & Henzinger, T. A. (2006). Executable biology (pp. 1675–1682).
Presented at the WSC: Winter Simulation Conference, IEEE. https://doi.org/10.1109/WSC.2006.322942'
chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Biology,” 1675–82.
IEEE, 2006. https://doi.org/10.1109/WSC.2006.322942.
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.'
mla: Fisher, Jasmin, and Thomas A. Henzinger. Executable Biology. IEEE, 2006,
pp. 1675–82, doi:10.1109/WSC.2006.322942.
short: J. Fisher, T.A. Henzinger, in:, IEEE, 2006, pp. 1675–1682.
conference:
name: 'WSC: Winter Simulation Conference'
date_created: 2018-12-11T12:09:19Z
date_published: 2006-12-03T00:00:00Z
date_updated: 2021-01-12T07:59:28Z
day: '03'
doi: 10.1109/WSC.2006.322942
extern: 1
month: '12'
page: 1675 - 1682
publication_status: published
publisher: IEEE
publist_id: '197'
quality_controlled: 0
status: public
title: Executable biology
type: conference
year: '2006'
...
---
_id: '4538'
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.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Strategy improvement and randomized subexponential
algorithms for stochastic parity games. In: Vol 3884. Springer; 2006:512-523.
doi:10.1007/11672142_42'
apa: 'Chatterjee, K., & 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. https://doi.org/10.1007/11672142_42'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games,” 3884:512–23.
Springer, 2006. https://doi.org/10.1007/11672142_42.
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.'
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.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Strategy Improvement and
Randomized Subexponential Algorithms for Stochastic Parity Games. Vol. 3884,
Springer, 2006, pp. 512–23, doi:10.1007/11672142_42.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 512–523.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '14'
doi: 10.1007/11672142_42
extern: 1
intvolume: ' 3884'
month: '02'
page: 512 - 523
publication_status: published
publisher: Springer
publist_id: '184'
quality_controlled: 0
status: public
title: Strategy improvement and randomized subexponential algorithms for stochastic
parity games
type: conference
volume: 3884
year: '2006'
...
---
_id: '4539'
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.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Finitary winning in omega-regular games. In: Vol
3920. Springer; 2006:257-271. doi:10.1007/11691372_17'
apa: 'Chatterjee, K., & 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. https://doi.org/10.1007/11691372_17'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Finitary Winning in Omega-Regular
Games,” 3920:257–71. Springer, 2006. https://doi.org/10.1007/11691372_17.
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.'
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.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Finitary Winning in Omega-Regular
Games. Vol. 3920, Springer, 2006, pp. 257–71, doi:10.1007/11691372_17.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2006, pp. 257–271.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2006-03-15T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '15'
doi: 10.1007/11691372_17
extern: 1
intvolume: ' 3920'
month: '03'
page: 257 - 271
publication_status: published
publisher: Springer
publist_id: '183'
quality_controlled: 0
status: public
title: Finitary winning in omega-regular games
type: conference
volume: 3920
year: '2006'
...
---
_id: '4549'
abstract:
- lang: eng
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.
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.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Marco
full_name: Faella, Marco
last_name: Faella
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'Chatterjee K, De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M.
Compositional quantitative reasoning. In: IEEE; 2006:179-188. doi:10.1109/QEST.2006.11'
apa: 'Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R.,
& Stoelinga, M. (2006). Compositional quantitative reasoning (pp. 179–188).
Presented at the QEST: Quantitative Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.11'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Thomas A Henzinger,
Ritankar Majumdar, and Mariëlle Stoelinga. “Compositional Quantitative Reasoning,”
179–88. IEEE, 2006. https://doi.org/10.1109/QEST.2006.11.
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.'
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.'
mla: Chatterjee, Krishnendu, et al. Compositional Quantitative Reasoning.
IEEE, 2006, pp. 179–88, doi:10.1109/QEST.2006.11.
short: K. Chatterjee, L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga,
in:, IEEE, 2006, pp. 179–188.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-09-01T00:00:00Z
date_updated: 2021-01-12T07:59:37Z
day: '01'
doi: 10.1109/QEST.2006.11
extern: 1
month: '09'
page: 179 - 188
publication_status: published
publisher: IEEE
publist_id: '163'
quality_controlled: 0
status: public
title: Compositional quantitative reasoning
type: conference
year: '2006'
...
---
_id: '4550'
abstract:
- lang: eng
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.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
citation:
ama: Chatterjee K, Henzinger TA, Jurdziński M. Games with secure equilibria. Theoretical
Computer Science. 2006;365(1-2):67-82. doi:10.1016/j.tcs.2006.07.032
apa: Chatterjee, K., Henzinger, T. A., & Jurdziński, M. (2006). Games with secure
equilibria. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2006.07.032
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Marcin Jurdziński. “Games
with Secure Equilibria.” Theoretical Computer Science. Elsevier, 2006.
https://doi.org/10.1016/j.tcs.2006.07.032.
ieee: K. Chatterjee, T. A. Henzinger, and M. Jurdziński, “Games with secure equilibria,”
Theoretical Computer Science, 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.
mla: Chatterjee, Krishnendu, et al. “Games with Secure Equilibria.” Theoretical
Computer Science, vol. 365, no. 1–2, Elsevier, 2006, pp. 67–82, doi:10.1016/j.tcs.2006.07.032.
short: K. Chatterjee, T.A. Henzinger, M. Jurdziński, Theoretical Computer Science
365 (2006) 67–82.
date_created: 2018-12-11T12:09:26Z
date_published: 2006-08-07T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '07'
doi: 10.1016/j.tcs.2006.07.032
extern: 1
intvolume: ' 365'
issue: 1-2
month: '08'
page: 67 - 82
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '164'
quality_controlled: 0
status: public
title: Games with secure equilibria
type: journal_article
volume: 365
year: '2006'
...
---
_id: '4551'
abstract:
- lang: eng
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. "
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.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Majumdar R, Henzinger TA. Markov decision processes with multiple
objectives. In: Vol 3884. Springer; 2006:325-336. doi:10.1007/11672142_26'
apa: 'Chatterjee, K., Majumdar, R., & 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. https://doi.org/10.1007/11672142_26'
chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Markov
Decision Processes with Multiple Objectives,” 3884:325–36. Springer, 2006. https://doi.org/10.1007/11672142_26.
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.'
mla: Chatterjee, Krishnendu, et al. Markov Decision Processes with Multiple Objectives.
Vol. 3884, Springer, 2006, pp. 325–36, doi:10.1007/11672142_26.
short: K. Chatterjee, R. Majumdar, T.A. Henzinger, in:, Springer, 2006, pp. 325–336.
conference:
name: 'STACS: Theoretical Aspects of Computer Science'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-02-14T00:00:00Z
date_updated: 2021-01-12T07:59:38Z
day: '14'
doi: 10.1007/11672142_26
extern: 1
intvolume: ' 3884'
month: '02'
page: 325 - 336
publication_status: published
publisher: Springer
publist_id: '161'
quality_controlled: 0
status: public
title: Markov decision processes with multiple objectives
type: conference
volume: 3884
year: '2006'
...
---
_id: '4552'
abstract:
- lang: eng
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 > 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.'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent
reachability games. In: IEEE; 2006:291-300. doi:10.1109/QEST.2006.48'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2006). Strategy improvement
for concurrent reachability games (pp. 291–300). Presented at the QEST: Quantitative
Evaluation of Systems, IEEE. https://doi.org/10.1109/QEST.2006.48'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy
Improvement for Concurrent Reachability Games,” 291–300. IEEE, 2006. https://doi.org/10.1109/QEST.2006.48.
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.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2006. Strategy improvement for concurrent
reachability games. QEST: Quantitative Evaluation of Systems, 291–300.'
mla: Chatterjee, Krishnendu, et al. Strategy Improvement for Concurrent Reachability
Games. IEEE, 2006, pp. 291–300, doi:10.1109/QEST.2006.48.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2006, pp. 291–300.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:26Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:39Z
day: '01'
doi: 10.1109/QEST.2006.48
extern: 1
month: '01'
page: 291 - 300
publication_status: published
publisher: IEEE
publist_id: '162'
quality_controlled: 0
status: public
title: Strategy improvement for concurrent reachability games
type: conference
year: '2006'
...
---
_id: '4574'
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.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G. Lazy shape analysis. In: Vol 4144. Springer;
2006:532-546. doi:10.1007/11817963_48'
apa: 'Beyer, D., Henzinger, T. A., & Théoduloz, G. (2006). Lazy shape analysis
(Vol. 4144, pp. 532–546). Presented at the CAV: Computer Aided Verification, Springer.
https://doi.org/10.1007/11817963_48'
chicago: Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Lazy Shape Analysis,”
4144:532–46. Springer, 2006. https://doi.org/10.1007/11817963_48.
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.'
mla: Beyer, Dirk, et al. Lazy Shape Analysis. Vol. 4144, Springer, 2006,
pp. 532–46, doi:10.1007/11817963_48.
short: D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2006, pp. 532–546.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:09:33Z
date_published: 2006-08-08T00:00:00Z
date_updated: 2021-01-12T07:59:49Z
day: '08'
doi: 10.1007/11817963_48
extern: 1
intvolume: ' 4144'
month: '08'
page: 532 - 546
publication_status: published
publisher: Springer
publist_id: '133'
quality_controlled: 0
status: public
title: Lazy shape analysis
type: conference
volume: 4144
year: '2006'
...
---
_id: '12657'
abstract:
- lang: eng
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.
article_processing_charge: No
article_type: original
author:
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: Ben
full_name: Brock, Ben
last_name: Brock
- first_name: Ulrich
full_name: Strasser, Ulrich
last_name: Strasser
- first_name: Paolo
full_name: Burlando, Paolo
last_name: Burlando
- first_name: Martin
full_name: Funk, Martin
last_name: Funk
- first_name: Javier
full_name: Corripio, Javier
last_name: Corripio
citation:
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. Journal of
Glaciology. 2005;51(175):573-587. doi:10.3189/172756505781829124'
apa: '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. Cambridge University Press. https://doi.org/10.3189/172756505781829124'
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.” Journal of Glaciology. Cambridge University Press, 2005.
https://doi.org/10.3189/172756505781829124.'
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,” Journal
of Glaciology, 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.'
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.” Journal of Glaciology, vol. 51, no. 175,
Cambridge University Press, 2005, pp. 573–87, doi:10.3189/172756505781829124.'
short: F. Pellicciotti, B. Brock, U. Strasser, P. Burlando, M. Funk, J. Corripio,
Journal of Glaciology 51 (2005) 573–587.
date_created: 2023-02-20T08:18:51Z
date_published: 2005-10-19T00:00:00Z
date_updated: 2023-02-20T08:45:37Z
day: '19'
doi: 10.3189/172756505781829124
extern: '1'
intvolume: ' 51'
issue: '175'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.3189/172756505781829124
month: '10'
oa: 1
oa_version: Published Version
page: 573-587
publication: Journal of Glaciology
publication_identifier:
eissn:
- 1727-5652
issn:
- 0022-1430
publication_status: published
publisher: Cambridge University Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'An enhanced temperature-index glacier melt model including the shortwave radiation
balance: Development and testing for Haut Glacier d’Arolla, Switzerland'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 51
year: '2005'
...
---
_id: '1298'
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.
acknowledgement: This work was supported by the Max-Planck-Society.
author:
- first_name: Dierk
full_name: Reiff, Dierk F
last_name: Reiff
- first_name: Alexandra
full_name: Ihring, Alexandra
last_name: Ihring
- first_name: Giovanna
full_name: Guerrero, Giovanna
last_name: Guerrero
- first_name: Ehud
full_name: Isacoff, Ehud Y
last_name: Isacoff
- first_name: Maximilian A
full_name: Maximilian Jösch
id: 2BD278E6-F248-11E8-B48F-1D18A9856A87
last_name: Jösch
orcid: 0000-0002-3937-1330
- first_name: Junichi
full_name: Nakai, Junichi
last_name: Nakai
- first_name: Alexander
full_name: Borst, Alexander
last_name: Borst
citation:
ama: Reiff D, Ihring A, Guerrero G, et al. In vivo performance of genetically encoded
indicators of neural activity in flies. Journal of Neuroscience. 2005;25(19):4766-4778.
doi:10.1523/JNEUROSCI.4900-04.2005
apa: Reiff, D., Ihring, A., Guerrero, G., Isacoff, E., Jösch, M. A., Nakai, J.,
& Borst, A. (2005). In vivo performance of genetically encoded indicators
of neural activity in flies. Journal of Neuroscience. Society for Neuroscience.
https://doi.org/10.1523/JNEUROSCI.4900-04.2005
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.” Journal of Neuroscience.
Society for Neuroscience, 2005. https://doi.org/10.1523/JNEUROSCI.4900-04.2005.
ieee: D. Reiff et al., “In vivo performance of genetically encoded indicators
of neural activity in flies,” Journal of Neuroscience, vol. 25, no. 19.
Society for Neuroscience, pp. 4766–4778, 2005.
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.
mla: Reiff, Dierk, et al. “In Vivo Performance of Genetically Encoded Indicators
of Neural Activity in Flies.” Journal of Neuroscience, vol. 25, no. 19,
Society for Neuroscience, 2005, pp. 4766–78, doi:10.1523/JNEUROSCI.4900-04.2005.
short: D. Reiff, A. Ihring, G. Guerrero, E. Isacoff, M.A. Jösch, J. Nakai, A. Borst,
Journal of Neuroscience 25 (2005) 4766–4778.
date_created: 2018-12-11T11:51:13Z
date_published: 2005-03-11T00:00:00Z
date_updated: 2021-01-12T06:49:42Z
day: '11'
doi: 10.1523/JNEUROSCI.4900-04.2005
extern: 1
intvolume: ' 25'
issue: '19'
month: '03'
page: 4766 - 4778
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '5975'
quality_controlled: 0
status: public
title: In vivo performance of genetically encoded indicators of neural activity in
flies
type: journal_article
volume: 25
year: '2005'
...
---
_id: '843'
abstract:
- lang: eng
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 >10-2, 10-2-10-4, 10-4-10-5 and <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.
author:
- first_name: Lev
full_name: Yampolsky, Lev Y
last_name: Yampolsky
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Alexey
full_name: Kondrashov, Alexey S
last_name: Kondrashov
citation:
ama: Yampolsky L, Kondrashov F, Kondrashov A. Distribution of the strength of selection
against amino acid replacements in human proteins. Human Molecular Genetics.
2005;14(21):3191-3201. doi:10.1093/hmg/ddi350
apa: Yampolsky, L., Kondrashov, F., & Kondrashov, A. (2005). Distribution of
the strength of selection against amino acid replacements in human proteins. Human
Molecular Genetics. Oxford University Press. https://doi.org/10.1093/hmg/ddi350
chicago: Yampolsky, Lev, Fyodor Kondrashov, and Alexey Kondrashov. “Distribution
of the Strength of Selection against Amino Acid Replacements in Human Proteins.”
Human Molecular Genetics. Oxford University Press, 2005. https://doi.org/10.1093/hmg/ddi350.
ieee: L. Yampolsky, F. Kondrashov, and A. Kondrashov, “Distribution of the strength
of selection against amino acid replacements in human proteins,” Human Molecular
Genetics, 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.
mla: Yampolsky, Lev, et al. “Distribution of the Strength of Selection against Amino
Acid Replacements in Human Proteins.” Human Molecular Genetics, vol. 14,
no. 21, Oxford University Press, 2005, pp. 3191–201, doi:10.1093/hmg/ddi350.
short: L. Yampolsky, F. Kondrashov, A. Kondrashov, Human Molecular Genetics 14 (2005)
3191–3201.
date_created: 2018-12-11T11:48:48Z
date_published: 2005-11-01T00:00:00Z
date_updated: 2021-01-12T08:19:13Z
day: '01'
doi: 10.1093/hmg/ddi350
extern: 1
intvolume: ' 14'
issue: '21'
month: '11'
page: 3191 - 3201
publication: Human Molecular Genetics
publication_status: published
publisher: Oxford University Press
publist_id: '6807'
quality_controlled: 0
status: public
title: Distribution of the strength of selection against amino acid replacements in
human proteins
type: journal_article
volume: 14
year: '2005'
...
---
_id: '8491'
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.
article_processing_charge: No
article_type: original
author:
- first_name: Paul
full_name: Schanda, Paul
id: 7B541462-FAF6-11E9-A490-E8DFE5697425
last_name: Schanda
orcid: 0000-0002-9350-7606
- first_name: Ēriks
full_name: Kupče, Ēriks
last_name: Kupče
- first_name: Bernhard
full_name: Brutscher, Bernhard
last_name: Brutscher
citation:
ama: Schanda P, Kupče Ē, Brutscher B. SOFAST-HMQC experiments for recording two-dimensional
deteronuclear correlation spectra of proteins within a few seconds. Journal
of Biomolecular NMR. 2005;33(4):199-211. doi:10.1007/s10858-005-4425-x
apa: 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. Springer Nature. https://doi.org/10.1007/s10858-005-4425-x
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.” Journal of Biomolecular NMR. Springer Nature, 2005. https://doi.org/10.1007/s10858-005-4425-x.
ieee: P. Schanda, Ē. Kupče, and B. Brutscher, “SOFAST-HMQC experiments for recording
two-dimensional deteronuclear correlation spectra of proteins within a few seconds,”
Journal of Biomolecular NMR, 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.” Journal
of Biomolecular NMR, vol. 33, no. 4, Springer Nature, 2005, pp. 199–211, doi:10.1007/s10858-005-4425-x.
short: P. Schanda, Ē. Kupče, B. Brutscher, Journal of Biomolecular NMR 33 (2005)
199–211.
date_created: 2020-09-18T10:13:59Z
date_published: 2005-12-01T00:00:00Z
date_updated: 2021-01-12T08:19:38Z
day: '01'
doi: 10.1007/s10858-005-4425-x
extern: '1'
intvolume: ' 33'
issue: '4'
keyword:
- Spectroscopy
- Biochemistry
language:
- iso: eng
month: '12'
oa_version: None
page: 199-211
publication: Journal of Biomolecular NMR
publication_identifier:
issn:
- 0925-2738
- 1573-5001
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: SOFAST-HMQC experiments for recording two-dimensional deteronuclear correlation
spectra of proteins within a few seconds
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 33
year: '2005'
...
---
_id: '8492'
abstract:
- lang: eng
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.
article_processing_charge: No
article_type: original
author:
- first_name: Paul
full_name: Schanda, Paul
id: 7B541462-FAF6-11E9-A490-E8DFE5697425
last_name: Schanda
orcid: 0000-0002-9350-7606
- first_name: Bernhard
full_name: Brutscher, Bernhard
last_name: Brutscher
citation:
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. Journal
of the American Chemical Society. 2005;127(22):8014-8015. doi:10.1021/ja051306e
apa: 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. American Chemical Society.
https://doi.org/10.1021/ja051306e
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.” Journal of the American Chemical Society. American Chemical Society,
2005. https://doi.org/10.1021/ja051306e.
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,”
Journal of the American Chemical Society, 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.
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.” Journal of the American Chemical Society, vol. 127, no. 22, American
Chemical Society, 2005, pp. 8014–15, doi:10.1021/ja051306e.
short: P. Schanda, B. Brutscher, Journal of the American Chemical Society 127 (2005)
8014–8015.
date_created: 2020-09-18T10:14:05Z
date_published: 2005-05-14T00:00:00Z
date_updated: 2021-01-12T08:19:39Z
day: '14'
doi: 10.1021/ja051306e
extern: '1'
intvolume: ' 127'
issue: '22'
keyword:
- Colloid and Surface Chemistry
- Biochemistry
- General Chemistry
- Catalysis
language:
- iso: eng
month: '05'
oa_version: None
page: 8014-8015
publication: Journal of the American Chemical Society
publication_identifier:
issn:
- 0002-7863
- 1520-5126
publication_status: published
publisher: American Chemical Society
quality_controlled: '1'
status: public
title: Very fast two-dimensional NMR spectroscopy for real-time investigation of dynamic
events in proteins on the time scale of seconds
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 127
year: '2005'
...
---
_id: '8516'
abstract:
- lang: eng
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."
article_processing_charge: No
article_type: original
author:
- first_name: Jean
full_name: Bourgain, Jean
last_name: Bourgain
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
citation:
ama: Bourgain J, Kaloshin V. On diffusion in high-dimensional Hamiltonian systems.
Journal of Functional Analysis. 2005;229(1):1-61. doi:10.1016/j.jfa.2004.09.006
apa: Bourgain, J., & Kaloshin, V. (2005). On diffusion in high-dimensional Hamiltonian
systems. Journal of Functional Analysis. Elsevier. https://doi.org/10.1016/j.jfa.2004.09.006
chicago: Bourgain, Jean, and Vadim Kaloshin. “On Diffusion in High-Dimensional Hamiltonian
Systems.” Journal of Functional Analysis. Elsevier, 2005. https://doi.org/10.1016/j.jfa.2004.09.006.
ieee: J. Bourgain and V. Kaloshin, “On diffusion in high-dimensional Hamiltonian
systems,” Journal of Functional Analysis, 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.” Journal of Functional Analysis, vol. 229, no. 1, Elsevier, 2005,
pp. 1–61, doi:10.1016/j.jfa.2004.09.006.
short: J. Bourgain, V. Kaloshin, Journal of Functional Analysis 229 (2005) 1–61.
date_created: 2020-09-18T10:49:06Z
date_published: 2005-12-01T00:00:00Z
date_updated: 2021-01-12T08:19:49Z
day: '01'
doi: 10.1016/j.jfa.2004.09.006
extern: '1'
intvolume: ' 229'
issue: '1'
keyword:
- Analysis
language:
- iso: eng
month: '12'
oa_version: None
page: 1-61
publication: Journal of Functional Analysis
publication_identifier:
issn:
- 0022-1236
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: On diffusion in high-dimensional Hamiltonian systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 229
year: '2005'
...