--- _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' ...