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