---
_id: '12640'
abstract:
- lang: eng
text: Greater Himalayan glaciers are retreating and losing mass at rates comparable
to glaciers in other regions of the world1,2,3,4,5. Assessments of future changes
and their associated hydrological impacts are scarce, oversimplify glacier dynamics
or include a limited number of climate models6,7,8,9. Here, we use results from
the latest ensemble of climate models in combination with a high-resolution glacio-hydrological
model to assess the hydrological impact of climate change on two climatically
contrasting watersheds in the Greater Himalaya, the Baltoro and Langtang watersheds
that drain into the Indus and Ganges rivers, respectively. We show that the largest
uncertainty in future runoff is a result of variations in projected precipitation
between climate models. In both watersheds, strong, but highly variable, increases
in future runoff are projected and, despite the different characteristics of the
watersheds, their responses are surprisingly similar. In both cases, glaciers
will recede but net glacier melt runoff is on a rising limb at least until 2050.
In combination with a positive change in precipitation, water availability during
this century is not likely to decline. We conclude that river basins that depend
on monsoon rains and glacier melt will continue to sustain the increasing water
demands expected in these areas10.
article_processing_charge: No
article_type: letter_note
author:
- first_name: W. W.
full_name: Immerzeel, W. W.
last_name: Immerzeel
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: M. F. P.
full_name: Bierkens, M. F. P.
last_name: Bierkens
citation:
ama: Immerzeel WW, Pellicciotti F, Bierkens MFP. Rising river flows throughout the
twenty-first century in two Himalayan glacierized watersheds. Nature Geoscience.
2013;6(9):742-745. doi:10.1038/ngeo1896
apa: Immerzeel, W. W., Pellicciotti, F., & Bierkens, M. F. P. (2013). Rising
river flows throughout the twenty-first century in two Himalayan glacierized watersheds.
Nature Geoscience. Springer Nature. https://doi.org/10.1038/ngeo1896
chicago: Immerzeel, W. W., Francesca Pellicciotti, and M. F. P. Bierkens. “Rising
River Flows throughout the Twenty-First Century in Two Himalayan Glacierized Watersheds.”
Nature Geoscience. Springer Nature, 2013. https://doi.org/10.1038/ngeo1896.
ieee: W. W. Immerzeel, F. Pellicciotti, and M. F. P. Bierkens, “Rising river flows
throughout the twenty-first century in two Himalayan glacierized watersheds,”
Nature Geoscience, vol. 6, no. 9. Springer Nature, pp. 742–745, 2013.
ista: Immerzeel WW, Pellicciotti F, Bierkens MFP. 2013. Rising river flows throughout
the twenty-first century in two Himalayan glacierized watersheds. Nature Geoscience.
6(9), 742–745.
mla: Immerzeel, W. W., et al. “Rising River Flows throughout the Twenty-First Century
in Two Himalayan Glacierized Watersheds.” Nature Geoscience, vol. 6, no.
9, Springer Nature, 2013, pp. 742–45, doi:10.1038/ngeo1896.
short: W.W. Immerzeel, F. Pellicciotti, M.F.P. Bierkens, Nature Geoscience 6 (2013)
742–745.
date_created: 2023-02-20T08:17:17Z
date_published: 2013-09-13T00:00:00Z
date_updated: 2023-02-21T10:46:37Z
day: '13'
doi: 10.1038/ngeo1896
extern: '1'
intvolume: ' 6'
issue: '9'
keyword:
- General Earth and Planetary Sciences
language:
- iso: eng
month: '09'
oa_version: None
page: 742-745
publication: Nature Geoscience
publication_identifier:
eissn:
- 1752-0908
issn:
- 1752-0894
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Rising river flows throughout the twenty-first century in two Himalayan glacierized
watersheds
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2013'
...
---
_id: '12641'
abstract:
- lang: eng
text: We investigate the sensitivity of a distributed enhanced temperature-index
(ETI) melt model, in order to understand which parameters have the largest influence
on model outputs and thus need to be accurately known. We use melt and meteorological
data from two Alpine glaciers and one glacier in the Andes of Chile. Sensitivity
analysis is conducted in a systematic way in terms of parameters and the different
conditions (day, night, clear-sky, overcast), melt seasons and glaciers examined.
The sensitivity of total melt to changes in individual parameters is calculated
using a local method around the optimal value of the parameters. We verify that
the parameters are optimal at the distributed scale and assess the model uncertainty
induced by uncertainty in the parameters using a Monte Carlo technique. Model
sensitivity to parameters is consistent across melt seasons, glaciers, different
conditions and the daily statistics examined. The parameters to which the model
is most sensitive are the shortwave-radiation factor, the temperature lapse rate
for extrapolation of air temperature, the albedo parameters, the temperature threshold
and the cloud transmittance factor parameters. A parameter uncertainty of 5% results
in a model uncertainty of 5.6% of mean melt on Haut Glacier d’Arolla, Switzerland.
article_processing_charge: No
article_type: original
author:
- first_name: Martin
full_name: Heynen, Martin
last_name: Heynen
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: Marco
full_name: Carenzo, Marco
last_name: Carenzo
citation:
ama: Heynen M, Pellicciotti F, Carenzo M. Parameter sensitivity of a distributed
enhanced temperature-index melt model. Annals of Glaciology. 2013;54(63):311-321.
doi:10.3189/2013aog63a537
apa: Heynen, M., Pellicciotti, F., & Carenzo, M. (2013). Parameter sensitivity
of a distributed enhanced temperature-index melt model. Annals of Glaciology.
International Glaciological Society. https://doi.org/10.3189/2013aog63a537
chicago: Heynen, Martin, Francesca Pellicciotti, and Marco Carenzo. “Parameter Sensitivity
of a Distributed Enhanced Temperature-Index Melt Model.” Annals of Glaciology.
International Glaciological Society, 2013. https://doi.org/10.3189/2013aog63a537.
ieee: M. Heynen, F. Pellicciotti, and M. Carenzo, “Parameter sensitivity of a distributed
enhanced temperature-index melt model,” Annals of Glaciology, vol. 54,
no. 63. International Glaciological Society, pp. 311–321, 2013.
ista: Heynen M, Pellicciotti F, Carenzo M. 2013. Parameter sensitivity of a distributed
enhanced temperature-index melt model. Annals of Glaciology. 54(63), 311–321.
mla: Heynen, Martin, et al. “Parameter Sensitivity of a Distributed Enhanced Temperature-Index
Melt Model.” Annals of Glaciology, vol. 54, no. 63, International Glaciological
Society, 2013, pp. 311–21, doi:10.3189/2013aog63a537.
short: M. Heynen, F. Pellicciotti, M. Carenzo, Annals of Glaciology 54 (2013) 311–321.
date_created: 2023-02-20T08:17:21Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2023-02-21T10:43:42Z
day: '01'
doi: 10.3189/2013aog63a537
extern: '1'
intvolume: ' 54'
issue: '63'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.3189/2013aog63a537
month: '08'
oa: 1
oa_version: Published Version
page: 311-321
publication: Annals of Glaciology
publication_identifier:
eissn:
- 1727-5644
issn:
- 0260-3055
publication_status: published
publisher: International Glaciological Society
quality_controlled: '1'
scopus_import: '1'
status: public
title: Parameter sensitivity of a distributed enhanced temperature-index melt model
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 54
year: '2013'
...
---
_id: '1304'
abstract:
- lang: eng
text: When confronted with a large-field stimulus rotating around the vertical body
axis, flies display a following behavior called "optomotor response."
As neural control elements, the large tangential horizontal system (HS) cells
of the lobula plate have been prime candidates for long. Here, we applied optogenetic
stimulation of HS cells to evaluate their behavioral role in Drosophila. To minimize
interference of the optical activation of channelrhodopsin-2 with the visual perception
of the flies, we used a bistable variant called ChR2-C128S. By applying pulses
of blue and yellow light, we first demonstrate electrophysiologically that lobula
plate tangential cells can be activated and deactivated repeatedly with no evident
change in depolarization strength over trials. We next show that selective optogenetic
activation of HS cells elicits robust yaw head movements and yaw turning responses
in fixed and tethered flying flies, respectively.
acknowledgement: 'This work was supported by the Max Planck Society. '
author:
- first_name: Väinö
full_name: Haikala, Väinö
last_name: Haikala
- 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: Alexander
full_name: Borst, Alexander
last_name: Borst
- first_name: Alex
full_name: Mauss, Alex S
last_name: Mauss
citation:
ama: Haikala V, Jösch MA, Borst A, Mauss A. Optogenetic control of fly optomotor
responses. Journal of Neuroscience. 2013;33(34):13927-13934. doi:10.1523/JNEUROSCI.0340-13.2013
apa: Haikala, V., Jösch, M. A., Borst, A., & Mauss, A. (2013). Optogenetic control
of fly optomotor responses. Journal of Neuroscience. Society for Neuroscience.
https://doi.org/10.1523/JNEUROSCI.0340-13.2013
chicago: Haikala, Väinö, Maximilian A Jösch, Alexander Borst, and Alex Mauss. “Optogenetic
Control of Fly Optomotor Responses.” Journal of Neuroscience. Society for
Neuroscience, 2013. https://doi.org/10.1523/JNEUROSCI.0340-13.2013.
ieee: V. Haikala, M. A. Jösch, A. Borst, and A. Mauss, “Optogenetic control of fly
optomotor responses,” Journal of Neuroscience, vol. 33, no. 34. Society
for Neuroscience, pp. 13927–13934, 2013.
ista: Haikala V, Jösch MA, Borst A, Mauss A. 2013. Optogenetic control of fly optomotor
responses. Journal of Neuroscience. 33(34), 13927–13934.
mla: Haikala, Väinö, et al. “Optogenetic Control of Fly Optomotor Responses.” Journal
of Neuroscience, vol. 33, no. 34, Society for Neuroscience, 2013, pp. 13927–34,
doi:10.1523/JNEUROSCI.0340-13.2013.
short: V. Haikala, M.A. Jösch, A. Borst, A. Mauss, Journal of Neuroscience 33 (2013)
13927–13934.
date_created: 2018-12-11T11:51:16Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:45Z
day: '01'
doi: 10.1523/JNEUROSCI.0340-13.2013
extern: 1
intvolume: ' 33'
issue: '34'
month: '01'
page: 13927 - 13934
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '5967'
quality_controlled: 0
status: public
title: Optogenetic control of fly optomotor responses
type: journal_article
volume: 33
year: '2013'
...
---
_id: '1305'
abstract:
- lang: eng
text: In the fly Drosophila melanogaster, photoreceptor input to motion vision is
split into two parallel pathways as represented by first-order interneurons L1
and L2 (Rister et al., 2007; Joesch et al., 2010). However, how these pathways
are functionally specialized remains controversial. One study (Eichner et al.,
2011) proposed that the L1-pathway evaluates only sequences of brightness increments
(ON-ON), while the L2-pathway processes exclusively brightness decrements (OFF-OFF).
Another study (Clark et al., 2011) proposed that each of the two pathways evaluates
both ON-ON and OFF-OFF sequences. To decide between these alternatives, we recorded
from motionsensitive neurons in flies in which the output from either L1 or L2
was genetically blocked. We found that blocking L1 abolishes ON-ON responses but
leaves OFF-OFF responses intact. The opposite was true, when the output from L2
was blocked. We conclude that the L1 and L2 pathways are functionally specialized
to detect ON-ON and OFF-OFF sequences, respectively.
acknowledgement: This work was supported by the Max-Planck-Society and the SFB 870
of the Deutsche Forschungsgemeinschaft.
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: Franz
full_name: Weber, Franz
last_name: Weber
- first_name: Hubert
full_name: Eichner, Hubert
last_name: Eichner
- first_name: Alexander
full_name: Borst, Alexander
last_name: Borst
citation:
ama: Jösch MA, Weber F, Eichner H, Borst A. Functional specialization of parallel
motion detection circuits in the fly. Journal of Neuroscience. 2013;33(3):902-905.
doi:10.1523/JNEUROSCI.3374-12.2013
apa: Jösch, M. A., Weber, F., Eichner, H., & Borst, A. (2013). Functional specialization
of parallel motion detection circuits in the fly. Journal of Neuroscience.
Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.3374-12.2013
chicago: Jösch, Maximilian A, Franz Weber, Hubert Eichner, and Alexander Borst.
“Functional Specialization of Parallel Motion Detection Circuits in the Fly.”
Journal of Neuroscience. Society for Neuroscience, 2013. https://doi.org/10.1523/JNEUROSCI.3374-12.2013.
ieee: M. A. Jösch, F. Weber, H. Eichner, and A. Borst, “Functional specialization
of parallel motion detection circuits in the fly,” Journal of Neuroscience,
vol. 33, no. 3. Society for Neuroscience, pp. 902–905, 2013.
ista: Jösch MA, Weber F, Eichner H, Borst A. 2013. Functional specialization of
parallel motion detection circuits in the fly. Journal of Neuroscience. 33(3),
902–905.
mla: Jösch, Maximilian A., et al. “Functional Specialization of Parallel Motion
Detection Circuits in the Fly.” Journal of Neuroscience, vol. 33, no. 3,
Society for Neuroscience, 2013, pp. 902–05, doi:10.1523/JNEUROSCI.3374-12.2013.
short: M.A. Jösch, F. Weber, H. Eichner, A. Borst, Journal of Neuroscience 33 (2013)
902–905.
date_created: 2018-12-11T11:51:16Z
date_published: 2013-01-16T00:00:00Z
date_updated: 2021-01-12T06:49:45Z
day: '16'
doi: 10.1523/JNEUROSCI.3374-12.2013
extern: 1
intvolume: ' 33'
issue: '3'
month: '01'
page: 902 - 905
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '5968'
quality_controlled: 0
status: public
title: Functional specialization of parallel motion detection circuits in the fly
type: journal_article
volume: 33
year: '2013'
...
---
_id: '1308'
abstract:
- lang: eng
text: We derive sufficient conditions for advection-driven backward motion of the
free boundary in a chemotaxis model with degenerate mobility. In this model, a
porous-medium-type diffusive term and an advection term are in competition. The
former induces forward motion, the latter may induce backward motion of the free
boundary depending on the direction of advection. We deduce conditions on the
growth of the initial data at the free boundary which ensure that at least initially
the advection term is dominant. This implies local backward motion of the free
boundary provided the advection is (locally) directed appropriately. Our result
is based on a new class of moving test functions and Stampacchia's lemma. As a
by-product of our estimates, we obtain quantitative bounds on the spreading of
the support of solutions for the chemotaxis model and provide a proof for the
finite speed of the support propagation property of solutions.
author:
- first_name: Julian L
full_name: Julian Fischer
id: 2C12A0B0-F248-11E8-B48F-1D18A9856A87
last_name: Fischer
orcid: 0000-0002-0479-558X
citation:
ama: Fischer JL. Advection-driven support shrinking in a chemotaxis model with degenerate
mobility. SIAM Journal on Mathematical Analysis. 2013;45(3):1585-1615.
doi:10.1137/120874291
apa: Fischer, J. L. (2013). Advection-driven support shrinking in a chemotaxis model
with degenerate mobility. SIAM Journal on Mathematical Analysis. Society
for Industrial and Applied Mathematics . https://doi.org/10.1137/120874291
chicago: Fischer, Julian L. “Advection-Driven Support Shrinking in a Chemotaxis
Model with Degenerate Mobility.” SIAM Journal on Mathematical Analysis.
Society for Industrial and Applied Mathematics , 2013. https://doi.org/10.1137/120874291.
ieee: J. L. Fischer, “Advection-driven support shrinking in a chemotaxis model with
degenerate mobility,” SIAM Journal on Mathematical Analysis, vol. 45, no.
3. Society for Industrial and Applied Mathematics , pp. 1585–1615, 2013.
ista: Fischer JL. 2013. Advection-driven support shrinking in a chemotaxis model
with degenerate mobility. SIAM Journal on Mathematical Analysis. 45(3), 1585–1615.
mla: Fischer, Julian L. “Advection-Driven Support Shrinking in a Chemotaxis Model
with Degenerate Mobility.” SIAM Journal on Mathematical Analysis, vol.
45, no. 3, Society for Industrial and Applied Mathematics , 2013, pp. 1585–615,
doi:10.1137/120874291.
short: J.L. Fischer, SIAM Journal on Mathematical Analysis 45 (2013) 1585–1615.
date_created: 2018-12-11T11:51:17Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:46Z
day: '01'
doi: 10.1137/120874291
extern: 1
intvolume: ' 45'
issue: '3'
month: '01'
page: 1585 - 1615
publication: SIAM Journal on Mathematical Analysis
publication_status: published
publisher: 'Society for Industrial and Applied Mathematics '
publist_id: '5963'
quality_controlled: 0
status: public
title: Advection-driven support shrinking in a chemotaxis model with degenerate mobility
type: journal_article
volume: 45
year: '2013'
...
---
_id: '1307'
abstract:
- lang: eng
text: We prove uniqueness of solutions of the DLSS equation in a class of sufficiently
regular functions. The global weak solutions of the DLSS equation constructed
by Jüngel and Matthes belong to this class of uniqueness. We also show uniqueness
of solutions for the quantum drift-diffusion equation, which contains additional
drift and second-order diffusion terms. The results hold in case of periodic or
Dirichlet-Neumann boundary conditions. Our proof is based on a monotonicity property
of the DLSS operator and sophisticated approximation arguments; we derive a PDE
satisfied by the pointwise square root of the solution, which enables us to exploit
the monotonicity property of the operator.
author:
- first_name: Julian L
full_name: Julian Fischer
id: 2C12A0B0-F248-11E8-B48F-1D18A9856A87
last_name: Fischer
orcid: 0000-0002-0479-558X
citation:
ama: Fischer JL. Uniqueness of solutions of the Derrida-Lebowitz-Speer-Spohn equation
and quantum drift diffusion models. Communications in Partial Differential
Equations. 2013;38(11):2004-2047. doi:10.1080/03605302.2013.823548
apa: Fischer, J. L. (2013). Uniqueness of solutions of the Derrida-Lebowitz-Speer-Spohn
equation and quantum drift diffusion models. Communications in Partial Differential
Equations. Taylor & Francis. https://doi.org/10.1080/03605302.2013.823548
chicago: Fischer, Julian L. “Uniqueness of Solutions of the Derrida-Lebowitz-Speer-Spohn
Equation and Quantum Drift Diffusion Models.” Communications in Partial Differential
Equations. Taylor & Francis, 2013. https://doi.org/10.1080/03605302.2013.823548.
ieee: J. L. Fischer, “Uniqueness of solutions of the Derrida-Lebowitz-Speer-Spohn
equation and quantum drift diffusion models,” Communications in Partial Differential
Equations, vol. 38, no. 11. Taylor & Francis, pp. 2004–2047, 2013.
ista: Fischer JL. 2013. Uniqueness of solutions of the Derrida-Lebowitz-Speer-Spohn
equation and quantum drift diffusion models. Communications in Partial Differential
Equations. 38(11), 2004–2047.
mla: Fischer, Julian L. “Uniqueness of Solutions of the Derrida-Lebowitz-Speer-Spohn
Equation and Quantum Drift Diffusion Models.” Communications in Partial Differential
Equations, vol. 38, no. 11, Taylor & Francis, 2013, pp. 2004–47, doi:10.1080/03605302.2013.823548.
short: J.L. Fischer, Communications in Partial Differential Equations 38 (2013)
2004–2047.
date_created: 2018-12-11T11:51:17Z
date_published: 2013-11-01T00:00:00Z
date_updated: 2021-01-12T06:49:46Z
day: '01'
doi: 10.1080/03605302.2013.823548
extern: 1
intvolume: ' 38'
issue: '11'
month: '11'
page: 2004 - 2047
publication: Communications in Partial Differential Equations
publication_status: published
publisher: Taylor & Francis
publist_id: '5962'
quality_controlled: 0
status: public
title: Uniqueness of solutions of the Derrida-Lebowitz-Speer-Spohn equation and quantum
drift diffusion models
type: journal_article
volume: 38
year: '2013'
...
---
_id: '1310'
abstract:
- lang: eng
text: We derive lower bounds on asymptotic support propagation rates for strong
solutions of the Cauchy problem for the thin-film equation. The bounds coincide
up to a constant factor with the previously known upper bounds and thus are sharp.
Our results hold in case of at most three spatial dimensions and n∈. (1, 2.92).
The result is established using weighted backward entropy inequalities with singular
weight functions to yield a differential inequality; combined with some entropy
production estimates, the optimal rate of propagation is obtained. To the best
of our knowledge, these are the first lower bounds on asymptotic support propagation
rates for higher-order nonnegativity-preserving parabolic equations.
author:
- first_name: Julian L
full_name: Julian Fischer
id: 2C12A0B0-F248-11E8-B48F-1D18A9856A87
last_name: Fischer
orcid: 0000-0002-0479-558X
citation:
ama: Fischer JL. Optimal lower bounds on asymptotic support propagation rates for
the thin-film equation. Journal of Differential Equations. 2013;255(10):3127-3149.
doi:10.1016/j.jde.2013.07.028
apa: Fischer, J. L. (2013). Optimal lower bounds on asymptotic support propagation
rates for the thin-film equation. Journal of Differential Equations. Academic
Press. https://doi.org/10.1016/j.jde.2013.07.028
chicago: Fischer, Julian L. “Optimal Lower Bounds on Asymptotic Support Propagation
Rates for the Thin-Film Equation.” Journal of Differential Equations. Academic
Press, 2013. https://doi.org/10.1016/j.jde.2013.07.028.
ieee: J. L. Fischer, “Optimal lower bounds on asymptotic support propagation rates
for the thin-film equation,” Journal of Differential Equations, vol. 255,
no. 10. Academic Press, pp. 3127–3149, 2013.
ista: Fischer JL. 2013. Optimal lower bounds on asymptotic support propagation rates
for the thin-film equation. Journal of Differential Equations. 255(10), 3127–3149.
mla: Fischer, Julian L. “Optimal Lower Bounds on Asymptotic Support Propagation
Rates for the Thin-Film Equation.” Journal of Differential Equations, vol.
255, no. 10, Academic Press, 2013, pp. 3127–49, doi:10.1016/j.jde.2013.07.028.
short: J.L. Fischer, Journal of Differential Equations 255 (2013) 3127–3149.
date_created: 2018-12-11T11:51:18Z
date_published: 2013-11-15T00:00:00Z
date_updated: 2021-01-12T06:49:47Z
day: '15'
doi: 10.1016/j.jde.2013.07.028
extern: 1
intvolume: ' 255'
issue: '10'
month: '11'
page: 3127 - 3149
publication: Journal of Differential Equations
publication_status: published
publisher: Academic Press
publist_id: '5961'
quality_controlled: 0
status: public
title: Optimal lower bounds on asymptotic support propagation rates for the thin-film
equation
type: journal_article
volume: 255
year: '2013'
...
---
_id: '1374'
abstract:
- lang: eng
text: 'We study two-player zero-sum games over infinite-state graphs equipped with
ωB and finitary conditions. Our first contribution is about the strategy complexity,
i.e the memory required for winning strategies: we prove that over general infinite-state
graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory
suffices for finitary parity games. We then study pushdown games with boundedness
conditions, with two contributions. First we prove a collapse result for pushdown
games with ωB-conditions, implying the decidability of solving these games. Second
we consider pushdown games with finitary parity along with stack boundedness conditions,
and show that solving these games is EXPTIME-complete.'
alternative_title:
- LIPIcs
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Nathanaël
full_name: Fijalkow, Nathanaël
last_name: Fijalkow
citation:
ama: 'Chatterjee K, Fijalkow N. Infinite-state games with finitary conditions. In:
22nd EACSL Annual Conference on Computer Science Logic. Vol 23. Leibniz
International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik; 2013:181-196. doi:10.4230/LIPIcs.CSL.2013.181'
apa: 'Chatterjee, K., & Fijalkow, N. (2013). Infinite-state games with finitary
conditions. In 22nd EACSL Annual Conference on Computer Science Logic (Vol.
23, pp. 181–196). Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CSL.2013.181'
chicago: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with
Finitary Conditions.” In 22nd EACSL Annual Conference on Computer Science Logic,
23:181–96. Leibniz International Proceedings in Informatics. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.181.
ieee: K. Chatterjee and N. Fijalkow, “Infinite-state games with finitary conditions,”
in 22nd EACSL Annual Conference on Computer Science Logic, Torino, Italy,
2013, vol. 23, pp. 181–196.
ista: 'Chatterjee K, Fijalkow N. 2013. Infinite-state games with finitary conditions.
22nd EACSL Annual Conference on Computer Science Logic. CSL: Computer Science
LogicLeibniz International Proceedings in Informatics, LIPIcs, vol. 23, 181–196.'
mla: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with
Finitary Conditions.” 22nd EACSL Annual Conference on Computer Science Logic,
vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–96,
doi:10.4230/LIPIcs.CSL.2013.181.
short: K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer
Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.
conference:
end_date: 2013-09-05
location: Torino, Italy
name: 'CSL: Computer Science Logic'
start_date: 203-09-02
date_created: 2018-12-11T11:51:39Z
date_published: 2013-09-01T00:00:00Z
date_updated: 2021-01-12T06:50:14Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CSL.2013.181
ec_funded: 1
file:
- access_level: open_access
checksum: b7091a3866db573c0db5ec486952255e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:38Z
date_updated: 2020-07-14T12:44:47Z
file_id: '5023'
file_name: IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf
file_size: 547296
relation: main_file
file_date_updated: 2020-07-14T12:44:47Z
has_accepted_license: '1'
intvolume: ' 23'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 181 - 196
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 22nd EACSL Annual Conference on Computer Science Logic
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5837'
pubrep_id: '624'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: Infinite-state games with finitary conditions
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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 23
year: '2013'
...
---
_id: '1385'
abstract:
- lang: eng
text: It is often difficult to correctly implement a Boolean controller for a complex
system, especially when concurrency is involved. Yet, it may be easy to formally
specify a controller. For instance, for a pipelined processor it suffices to state
that the visible behavior of the pipelined system should be identical to a non-pipelined
reference system (Burch-Dill paradigm). We present a novel procedure to efficiently
synthesize multiple Boolean control signals from a specification given as a quantified
first-order formula (with a specific quantifier structure). Our approach uses
uninterpreted functions to abstract details of the design. We construct an unsatisfiable
SMT formula from the given specification. Then, from just one proof of unsatisfiability,
we use a variant of Craig interpolation to compute multiple coordinated interpolants
that implement the Boolean control signals. Our method avoids iterative learning
and back-substitution of the control functions. We applied our approach to synthesize
a controller for a simple two-stage pipelined processor, and present first experimental
results.
acknowledgement: "This research was supported by the European Commission through project\r\nDIAMOND
\ (FP7-2009-IST-4-248613), and QUAINT (I774-N23), "
author:
- first_name: Georg
full_name: Hofferek, Georg
last_name: Hofferek
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Jie
full_name: Jiang, Jie
last_name: Jiang
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
citation:
ama: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple
boolean functions using interpolation on a single proof. In: 2013 Formal Methods
in Computer-Aided Design. IEEE; 2013:77-84. doi:10.1109/FMCAD.2013.6679394'
apa: 'Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., & Bloem, R. (2013).
Synthesizing multiple boolean functions using interpolation on a single proof.
In 2013 Formal Methods in Computer-Aided Design (pp. 77–84). Portland,
OR, United States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679394'
chicago: Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick
Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single
Proof.” In 2013 Formal Methods in Computer-Aided Design, 77–84. IEEE, 2013.
https://doi.org/10.1109/FMCAD.2013.6679394.
ieee: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing
multiple boolean functions using interpolation on a single proof,” in 2013
Formal Methods in Computer-Aided Design, Portland, OR, United States, 2013,
pp. 77–84.
ista: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple
boolean functions using interpolation on a single proof. 2013 Formal Methods in
Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84.'
mla: Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation
on a Single Proof.” 2013 Formal Methods in Computer-Aided Design, IEEE,
2013, pp. 77–84, doi:10.1109/FMCAD.2013.6679394.
short: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal
Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.
conference:
end_date: 2013-10-23
location: Portland, OR, United States
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2013-10-20
date_created: 2018-12-11T11:51:43Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2021-01-12T06:50:19Z
day: '11'
department:
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679394
ec_funded: 1
external_id:
arxiv:
- '1308.4767'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1308.4767
month: '12'
oa: 1
oa_version: Preprint
page: 77 - 84
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: 2013 Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5825'
quality_controlled: '1'
status: public
title: Synthesizing multiple boolean functions using interpolation on a single proof
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1387'
abstract:
- lang: eng
text: Choices made by nondeterministic word automata depend on both the past (the
prefix of the word read so far) and the future (the suffix yet to be read). In
several applications, most notably synthesis, the future is diverse or unknown,
leading to algorithms that are based on deterministic automata. Hoping to retain
some of the advantages of nondeterministic automata, researchers have studied
restricted classes of nondeterministic automata. Three such classes are nondeterministic
automata that are good for trees (GFT; i.e., ones that can be expanded to tree
automata accepting the derived tree languages, thus whose choices should satisfy
diverse futures), good for games (GFG; i.e., ones whose choices depend only on
the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent
deterministic automata). The theoretical properties and relative merits of the
different classes are still open, having vagueness on whether they really differ
from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known
whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also
open is the possible succinctness of GFG and GFT automata compared to deterministic
automata. We study these problems for ω-regular automata with all common acceptance
conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction
for GFG automata.
acknowledgement: and ERC Grant QUALITY.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Denis
full_name: Kuperberg, Denis
last_name: Kuperberg
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Michał
full_name: Skrzypczak, Michał
last_name: Skrzypczak
citation:
ama: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. Nondeterminism in the presence
of a diverse or unknown future. 2013;7966(PART 2):89-100. doi:10.1007/978-3-642-39212-2_11
apa: 'Boker, U., Kuperberg, D., Kupferman, O., & Skrzypczak, M. (2013). Nondeterminism
in the presence of a diverse or unknown future. Presented at the ICALP: Automata,
Languages and Programming, Riga, Latvia: Springer. https://doi.org/10.1007/978-3-642-39212-2_11'
chicago: Boker, Udi, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. “Nondeterminism
in the Presence of a Diverse or Unknown Future.” Lecture Notes in Computer Science.
Springer, 2013. https://doi.org/10.1007/978-3-642-39212-2_11.
ieee: U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak, “Nondeterminism in
the presence of a diverse or unknown future,” vol. 7966, no. PART 2. Springer,
pp. 89–100, 2013.
ista: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. 2013. Nondeterminism in the
presence of a diverse or unknown future. 7966(PART 2), 89–100.
mla: Boker, Udi, et al. Nondeterminism in the Presence of a Diverse or Unknown
Future. Vol. 7966, no. PART 2, Springer, 2013, pp. 89–100, doi:10.1007/978-3-642-39212-2_11.
short: U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.
conference:
end_date: 2013-07-12
location: Riga, Latvia
name: 'ICALP: Automata, Languages and Programming'
start_date: 2013-07-08
date_created: 2018-12-11T11:51:44Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:09Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39212-2_11
ec_funded: 1
file:
- access_level: open_access
checksum: 98bc02e3793072e279ec8d364b381ff3
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T11:05:50Z
date_updated: 2020-07-14T12:44:48Z
file_id: '7857'
file_name: 2013_ICALP_Boker.pdf
file_size: 276982
relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: ' 7966'
issue: PART 2
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 89 - 100
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5823'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Nondeterminism in the presence of a diverse or unknown future
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7966
year: '2013'
...