[{"volume":13994,"publication_status":"published","publication_identifier":{"isbn":["9783031308192"],"eissn":["1611-3349"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"file":[{"file_id":"13151","checksum":"60dcafc1b4f6f070be43bad3fe877974","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2023-06-19T08:43:21Z","file_name":"2023_LNCS_Anand.pdf","date_updated":"2023-06-19T08:43:21Z","file_size":521425,"creator":"dernst"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 13994","month":"04","abstract":[{"text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.","lang":"eng"}],"oa_version":"Published Version","department":[{"_id":"ToHe"}],"file_date_updated":"2023-06-19T08:43:21Z","date_updated":"2023-06-19T08:49:46Z","ddc":["000"],"conference":{"start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","status":"public","_id":"13141","page":"211-228","date_created":"2023-06-18T22:00:47Z","doi":"10.1007/978-3-031-30820-8_15","date_published":"2023-04-20T00:00:00Z","year":"2023","has_accepted_license":"1","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","day":"20","oa":1,"publisher":"Springer Nature","quality_controlled":"1","article_processing_charge":"No","author":[{"last_name":"Anand","full_name":"Anand, Ashwani","first_name":"Ashwani"},{"first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","last_name":"Mallik"},{"full_name":"Nayak, Satya Prakash","last_name":"Nayak","first_name":"Satya Prakash"},{"first_name":"Anne Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin"}],"title":"Computing adequately permissive assumptions for synthesis","citation":{"chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228.","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.","short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 211–228.","apa":"Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15","ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"ec_funded":1,"publication_identifier":{"issn":["2663 - 337X"]},"degree_awarded":"PhD","publication_status":"published","file":[{"content_type":"application/vnd.openxmlformats-officedocument.wordprocessingml.document","access_level":"closed","relation":"source_file","file_id":"12857","checksum":"5f589a9af025f7eeebfd0c186209913e","date_updated":"2023-04-20T09:26:51Z","file_size":14507243,"creator":"vpokusae","date_created":"2023-04-20T09:14:38Z","file_name":"Thesis_Pokusaeva.docx"},{"date_created":"2023-04-20T09:14:44Z","file_name":"Thesis_Pokusaeva.pdf","date_updated":"2023-04-20T09:14:44Z","file_size":10090711,"creator":"vpokusae","file_id":"12858","checksum":"bbeed76db45a996b4c91a9abe12ce0ec","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"alternative_title":["ISTA Thesis"],"month":"04","abstract":[{"text":"During navigation, animals can infer the structure of the environment by computing the optic flow cues elicited by their own movements, and subsequently use this information to instruct proper locomotor actions. These computations require a panoramic assessment of the visual environment in order to disambiguate similar sensory experiences that may require distinct behavioral responses. The estimation of the global motion patterns is therefore essential for successful navigation. Yet, our understanding of the algorithms and implementations that enable coherent panoramic visual perception remains scarce. Here I pursue this problem by dissecting the functional aspects of interneuronal communication in the lobula plate tangential cell network in Drosophila melanogaster. The results presented in the thesis demonstrate that the basis for effective interpretation of the optic flow in this circuit are stereotyped synaptic connections that mediate the formation of distinct subnetworks, each extracting a particular pattern of global motion. \r\nFirstly, I show that gap junctions are essential for a correct interpretation of binocular motion cues by horizontal motion-sensitive cells. HS cells form electrical synapses with contralateral H2 neurons that are involved in detecting yaw rotation and translation. I developed an FlpStop-mediated mutant of a gap junction protein ShakB that disrupts these electrical synapses. While the loss of electrical synapses does not affect the tuning of the direction selectivity in HS neurons, it severely alters their sensitivity to horizontal motion in the contralateral side. These physiological changes result in an inappropriate integration of binocular motion cues in walking animals. While wild-type flies form a binocular perception of visual motion by non-linear integration of monocular optic flow cues, the mutant flies sum the monocular inputs linearly. These results indicate that rather than averaging signals in neighboring neurons, gap-junctions operate in conjunction with chemical synapses to mediate complex non-linear optic flow computations.\r\nSecondly, I show that stochastic manipulation of neuronal activity in the lobula plate tangential cell network is a powerful approach to study the neuronal implementation of optic flow-based navigation in flies. Tangential neurons form multiple subnetworks, each mediating course-stabilizing response to a particular global pattern of visual motion. Application of genetic mosaic techniques can provide sparse optogenetic activation of HS cells in numerous combinations. These distinct combinations of activated neurons drive an array of distinct behavioral responses, providing important insights into how visuomotor transformation is performed in the lobula plate tangential cell network. This approach can be complemented by stochastic silencing of tangential neurons, enabling direct assessment of the functional role of individual tangential neurons in the processing of specific visual motion patterns.\r\n\tTaken together, the findings presented in this thesis suggest that establishing specific activity patterns of tangential cells via stereotyped synaptic connectivity is a key to efficient optic flow-based navigation in Drosophila melanogaster.","lang":"eng"}],"acknowledged_ssus":[{"_id":"Bio"},{"_id":"LifeSc"}],"oa_version":"Published Version","department":[{"_id":"MaJö"},{"_id":"GradSch"}],"file_date_updated":"2023-04-20T09:26:51Z","supervisor":[{"last_name":"Jösch","orcid":"0000-0002-3937-1330","full_name":"Jösch, Maximilian A","id":"2BD278E6-F248-11E8-B48F-1D18A9856A87","first_name":"Maximilian A"}],"date_updated":"2023-06-23T09:47:36Z","ddc":["570","571"],"type":"dissertation","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","_id":"12826","page":"106","date_published":"2023-04-18T00:00:00Z","doi":"10.15479/at:ista:12826","date_created":"2023-04-14T14:56:04Z","has_accepted_license":"1","year":"2023","day":"18","publisher":"Institute of Science and Technology Austria","oa":1,"author":[{"orcid":"0000-0001-7660-444X","full_name":"Pokusaeva, Victoria","last_name":"Pokusaeva","first_name":"Victoria","id":"3184041C-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","title":"Neural control of optic flow-based navigation in Drosophila melanogaster","citation":{"chicago":"Pokusaeva, Victoria. “Neural Control of Optic Flow-Based Navigation in Drosophila Melanogaster.” Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/at:ista:12826.","ista":"Pokusaeva V. 2023. Neural control of optic flow-based navigation in Drosophila melanogaster. Institute of Science and Technology Austria.","mla":"Pokusaeva, Victoria. Neural Control of Optic Flow-Based Navigation in Drosophila Melanogaster. Institute of Science and Technology Austria, 2023, doi:10.15479/at:ista:12826.","ama":"Pokusaeva V. Neural control of optic flow-based navigation in Drosophila melanogaster. 2023. doi:10.15479/at:ista:12826","apa":"Pokusaeva, V. (2023). Neural control of optic flow-based navigation in Drosophila melanogaster. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:12826","short":"V. Pokusaeva, Neural Control of Optic Flow-Based Navigation in Drosophila Melanogaster, Institute of Science and Technology Austria, 2023.","ieee":"V. Pokusaeva, “Neural control of optic flow-based navigation in Drosophila melanogaster,” Institute of Science and Technology Austria, 2023."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","project":[{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}]},{"article_processing_charge":"Yes (via OA deal)","external_id":{"isi":["000846967100001"]},"author":[{"orcid":"0000-0002-9823-6833","full_name":"Edelsbrunner, Herbert","last_name":"Edelsbrunner","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","first_name":"Herbert"},{"full_name":"Osang, Georg F","last_name":"Osang","first_name":"Georg F","id":"464B40D6-F248-11E8-B48F-1D18A9856A87"}],"title":"A simple algorithm for higher-order Delaunay mosaics and alpha shapes","citation":{"ista":"Edelsbrunner H, Osang GF. 2023. A simple algorithm for higher-order Delaunay mosaics and alpha shapes. Algorithmica. 85, 277–295.","chicago":"Edelsbrunner, Herbert, and Georg F Osang. “A Simple Algorithm for Higher-Order Delaunay Mosaics and Alpha Shapes.” Algorithmica. Springer Nature, 2023. https://doi.org/10.1007/s00453-022-01027-6.","apa":"Edelsbrunner, H., & Osang, G. F. (2023). A simple algorithm for higher-order Delaunay mosaics and alpha shapes. Algorithmica. Springer Nature. https://doi.org/10.1007/s00453-022-01027-6","ama":"Edelsbrunner H, Osang GF. A simple algorithm for higher-order Delaunay mosaics and alpha shapes. Algorithmica. 2023;85:277-295. doi:10.1007/s00453-022-01027-6","ieee":"H. Edelsbrunner and G. F. Osang, “A simple algorithm for higher-order Delaunay mosaics and alpha shapes,” Algorithmica, vol. 85. Springer Nature, pp. 277–295, 2023.","short":"H. Edelsbrunner, G.F. Osang, Algorithmica 85 (2023) 277–295.","mla":"Edelsbrunner, Herbert, and Georg F. Osang. “A Simple Algorithm for Higher-Order Delaunay Mosaics and Alpha Shapes.” Algorithmica, vol. 85, Springer Nature, 2023, pp. 277–95, doi:10.1007/s00453-022-01027-6."},"user_id":"2EBD1598-F248-11E8-B48F-1D18A9856A87","project":[{"name":"Alpha Shape Theory Extended","grant_number":"788183","call_identifier":"H2020","_id":"266A2E9E-B435-11E9-9278-68D0E5697425"},{"_id":"268116B8-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z00342"},{"call_identifier":"FWF","_id":"2561EBF4-B435-11E9-9278-68D0E5697425","grant_number":"I02979-N35","name":"Persistence and stability of geometric complexes"}],"page":"277-295","date_created":"2022-09-11T22:01:57Z","date_published":"2023-01-01T00:00:00Z","doi":"10.1007/s00453-022-01027-6","year":"2023","isi":1,"has_accepted_license":"1","publication":"Algorithmica","day":"01","oa":1,"quality_controlled":"1","publisher":"Springer Nature","acknowledgement":"Open access funding provided by Austrian Science Fund (FWF). This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, Grant No. 788183, from the Wittgenstein Prize, Austrian Science Fund (FWF), Grant No. Z 342-N31, and from the DFG Collaborative Research Center TRR 109, ‘Discretization in Geometry and Dynamics’, Austrian Science Fund (FWF), Grant No. I 02979-N35.","file_date_updated":"2023-01-20T10:02:48Z","department":[{"_id":"HeEd"}],"date_updated":"2023-06-27T12:53:43Z","ddc":["510"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","article_type":"original","status":"public","_id":"12086","ec_funded":1,"volume":85,"publication_status":"published","publication_identifier":{"eissn":["1432-0541"],"issn":["0178-4617"]},"language":[{"iso":"eng"}],"file":[{"file_name":"2023_Algorithmica_Edelsbrunner.pdf","date_created":"2023-01-20T10:02:48Z","file_size":911017,"date_updated":"2023-01-20T10:02:48Z","creator":"dernst","success":1,"file_id":"12322","checksum":"71685ca5121f4c837f40c3f8eb50c915","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"scopus_import":"1","intvolume":" 85","month":"01","abstract":[{"lang":"eng","text":"We present a simple algorithm for computing higher-order Delaunay mosaics that works in Euclidean spaces of any finite dimensions. The algorithm selects the vertices of the order-k mosaic from incrementally constructed lower-order mosaics and uses an algorithm for weighted first-order Delaunay mosaics as a black-box to construct the order-k mosaic from its vertices. Beyond this black-box, the algorithm uses only combinatorial operations, thus facilitating easy implementation. We extend this algorithm to compute higher-order α-shapes and provide open-source implementations. We present experimental results for properties of higher-order Delaunay mosaics of random point sets."}],"oa_version":"Published Version"},{"acknowledgement":"Research supported by the Austrian Science Fund (FWF) grant F65 at the Institute of Science and Technology Austria and by the European Research Council (ERC) (Grant agreement No. 716117 awarded to Prof. Dr. Jan Maas). L.D.S. gratefully acknowledges funding of his current position by the Austrian Science Fund (FWF) through the ESPRIT Programme (Grant No. 208). M.W. gratefully acknowledges funding of his current position by the Austrian Science Fund (FWF) through the ESPRIT Programme (Grant No. 156).","publisher":"Springer Nature","quality_controlled":"1","oa":1,"day":"01","publication":"Journal of Evolution Equations","has_accepted_license":"1","isi":1,"year":"2023","date_published":"2023-01-01T00:00:00Z","doi":"10.1007/s00028-022-00859-7","date_created":"2023-01-08T23:00:53Z","article_number":"9","project":[{"grant_number":"F6504","name":"Taming Complexity in Partial Differential Systems","_id":"fc31cba2-9c52-11eb-aca3-ff467d239cd2"},{"call_identifier":"H2020","_id":"256E75B8-B435-11E9-9278-68D0E5697425","grant_number":"716117","name":"Optimal Transport and Stochastic Dynamics"},{"name":"Configuration Spaces over Non-Smooth Spaces","grant_number":"E208","_id":"34dbf174-11ca-11ed-8bc3-afe9d43d4b9c"},{"grant_number":"ESP156_N","name":"Gradient flow techniques for quantum Markov semigroups","_id":"34c6ea2d-11ca-11ed-8bc3-c04f3c502833"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Dello Schiavo, Lorenzo, and Melchior Wirth. “Ergodic Decompositions of Dirichlet Forms under Order Isomorphisms.” Journal of Evolution Equations, vol. 23, no. 1, 9, Springer Nature, 2023, doi:10.1007/s00028-022-00859-7.","apa":"Dello Schiavo, L., & Wirth, M. (2023). Ergodic decompositions of Dirichlet forms under order isomorphisms. Journal of Evolution Equations. Springer Nature. https://doi.org/10.1007/s00028-022-00859-7","ama":"Dello Schiavo L, Wirth M. Ergodic decompositions of Dirichlet forms under order isomorphisms. Journal of Evolution Equations. 2023;23(1). doi:10.1007/s00028-022-00859-7","short":"L. Dello Schiavo, M. Wirth, Journal of Evolution Equations 23 (2023).","ieee":"L. Dello Schiavo and M. Wirth, “Ergodic decompositions of Dirichlet forms under order isomorphisms,” Journal of Evolution Equations, vol. 23, no. 1. Springer Nature, 2023.","chicago":"Dello Schiavo, Lorenzo, and Melchior Wirth. “Ergodic Decompositions of Dirichlet Forms under Order Isomorphisms.” Journal of Evolution Equations. Springer Nature, 2023. https://doi.org/10.1007/s00028-022-00859-7.","ista":"Dello Schiavo L, Wirth M. 2023. Ergodic decompositions of Dirichlet forms under order isomorphisms. Journal of Evolution Equations. 23(1), 9."},"title":"Ergodic decompositions of Dirichlet forms under order isomorphisms","author":[{"id":"ECEBF480-9E4F-11EA-B557-B0823DDC885E","first_name":"Lorenzo","orcid":"0000-0002-9881-6870","full_name":"Dello Schiavo, Lorenzo","last_name":"Dello Schiavo"},{"orcid":"0000-0002-0519-4241","full_name":"Wirth, Melchior","last_name":"Wirth","first_name":"Melchior","id":"88644358-0A0E-11EA-8FA5-49A33DDC885E"}],"external_id":{"isi":["000906214600004"]},"article_processing_charge":"Yes (via OA deal)","oa_version":"Published Version","abstract":[{"text":"We study ergodic decompositions of Dirichlet spaces under intertwining via unitary order isomorphisms. We show that the ergodic decomposition of a quasi-regular Dirichlet space is unique up to a unique isomorphism of the indexing space. Furthermore, every unitary order isomorphism intertwining two quasi-regular Dirichlet spaces is decomposable over their ergodic decompositions up to conjugation via an isomorphism of the corresponding indexing spaces.","lang":"eng"}],"month":"01","intvolume":" 23","scopus_import":"1","file":[{"checksum":"1f34f3e2cb521033de6154f274ea3a4e","file_id":"12325","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2023-01-20T10:45:06Z","file_name":"2023_JourEvolutionEquations_DelloSchiavo.pdf","creator":"dernst","date_updated":"2023-01-20T10:45:06Z","file_size":422612}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["1424-3199"],"eissn":["1424-3202"]},"publication_status":"published","volume":23,"issue":"1","ec_funded":1,"_id":"12104","status":"public","article_type":"original","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["510"],"date_updated":"2023-06-28T11:54:35Z","department":[{"_id":"JaMa"}],"file_date_updated":"2023-01-20T10:45:06Z"},{"page":"427-442","date_created":"2022-06-05T22:01:50Z","doi":"10.1007/s00382-022-06337-7","date_published":"2023-01-01T00:00:00Z","year":"2023","isi":1,"publication":"Climate Dynamics","day":"01","publisher":"Springer Nature","quality_controlled":"1","acknowledgement":"This work was supported by the National Research Foundation of Korea (NRF) grant funded by the Korea government (MSIT) (NRF-2018R1A5A1024958). Model simulation and data transfer were supported by the National Supercomputing Center with supercomputing resources including technical support (KSC-2019-CHA-0005), the National Center for Meteorological Supercomputer of Korea Meteorological Administration, and by the Korea Research Environment Open NETwork (KREONET), respectively. The authors declare no conflicts of interest.","article_processing_charge":"No","external_id":{"isi":["000803119400002"]},"author":[{"last_name":"Goswami","full_name":"Goswami, Bidyut B","id":"3a4ac09c-6d61-11ec-bf66-884cde66b64b","first_name":"Bidyut B"}],"title":"Role of the eastern equatorial Indian Ocean warming in the Indian summer monsoon rainfall trend","citation":{"ama":"GOSWAMI BB. Role of the eastern equatorial Indian Ocean warming in the Indian summer monsoon rainfall trend. Climate Dynamics. 2023;60:427-442. doi:10.1007/s00382-022-06337-7","apa":"GOSWAMI, B. B. (2023). Role of the eastern equatorial Indian Ocean warming in the Indian summer monsoon rainfall trend. Climate Dynamics. Springer Nature. https://doi.org/10.1007/s00382-022-06337-7","short":"B.B. GOSWAMI, Climate Dynamics 60 (2023) 427–442.","ieee":"B. B. GOSWAMI, “Role of the eastern equatorial Indian Ocean warming in the Indian summer monsoon rainfall trend,” Climate Dynamics, vol. 60. Springer Nature, pp. 427–442, 2023.","mla":"GOSWAMI, BIDYUT B. “Role of the Eastern Equatorial Indian Ocean Warming in the Indian Summer Monsoon Rainfall Trend.” Climate Dynamics, vol. 60, Springer Nature, 2023, pp. 427–42, doi:10.1007/s00382-022-06337-7.","ista":"GOSWAMI BB. 2023. Role of the eastern equatorial Indian Ocean warming in the Indian summer monsoon rainfall trend. Climate Dynamics. 60, 427–442.","chicago":"GOSWAMI, BIDYUT B. “Role of the Eastern Equatorial Indian Ocean Warming in the Indian Summer Monsoon Rainfall Trend.” Climate Dynamics. Springer Nature, 2023. https://doi.org/10.1007/s00382-022-06337-7."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"link":[{"relation":"erratum","url":" https://doi.org/10.1007/s00382-022-06401-2"}]},"volume":60,"publication_status":"published","publication_identifier":{"eissn":["1432-0894"],"issn":["0930-7575"]},"language":[{"iso":"eng"}],"scopus_import":"1","intvolume":" 60","month":"01","abstract":[{"text":"The Indian summer monsoon rainfall (ISMR) has been declining since the 1950s. However, since 2002 it is reported to have revived. For these observed changes in the ISMR, several explanations have been reported. Among these explanations, however, the role of the eastern equatorial Indian Ocean (EEIO) is missing despite being one of the warmest regions in the Indian Ocean, and monotonously warming. A recent study reported that EEIO warming impacts the rainfall over northern India. Here we report that warming in the EEIO weakens the low-level Indian summer monsoon circulation and reduces ISMR. A warm EEIO drives easterly winds in the Indo–Pacific sector as a Gill response. The warm EEIO also enhances nocturnal convection offshore the western coast of Sumatra. The latent heating associated with the increased convection augments the Gill response and the resultant circulation opposes the monsoon low-level circulation and weakens the seasonal rainfall.","lang":"eng"}],"oa_version":"None","department":[{"_id":"CaMu"}],"date_updated":"2023-06-28T11:49:58Z","type":"journal_article","article_type":"original","status":"public","_id":"11434"},{"day":"21","publication":"26th International Conference Foundations of Software Science and Computation Structures","has_accepted_license":"1","year":"2023","doi":"10.1007/978-3-031-30829-1_17","date_published":"2023-04-21T00:00:00Z","date_created":"2023-01-31T07:23:56Z","page":"349-370","acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","publisher":"Springer Nature","quality_controlled":"1","oa":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in 26th International Conference Foundations of Software Science and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference Foundations of Software Science and Computation Structures, Springer Nature, 2023, pp. 349–370.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: 26th International Conference Foundations of Software Science and Computation Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17","apa":"Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative safety and liveness. In 26th International Conference Foundations of Software Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17","mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International Conference Foundations of Software Science and Computation Structures, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness. 26th International Conference Foundations of Software Science and Computation Structures. FOSSACS: Foundations of Software Science and Computation Structures, LNCS, vol. 13992, 349–370.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In 26th International Conference Foundations of Software Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17."},"title":"Quantitative safety and liveness","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi"},{"full_name":"Sarac, Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"article_processing_charge":"No","external_id":{"arxiv":["2301.11175"]},"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"file":[{"date_created":"2023-01-31T07:22:21Z","file_name":"qsl.pdf","creator":"esarac","date_updated":"2023-01-31T07:22:21Z","file_size":449027,"file_id":"12468","checksum":"981025aed580b6b27c426cb8856cf63e","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf"},{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"13153","checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","success":1,"date_updated":"2023-06-19T10:28:09Z","file_size":1048171,"creator":"dernst","date_created":"2023-06-19T10:28:09Z","file_name":"2023_LNCS_HenzingerT.pdf"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308284"],"eissn":["1611-3349"]},"publication_status":"published","volume":13992,"ec_funded":1,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states."}],"month":"04","intvolume":" 13992","alternative_title":["LNCS"],"scopus_import":"1","ddc":["000"],"date_updated":"2023-07-14T11:20:27Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"file_date_updated":"2023-06-19T10:28:09Z","_id":"12467","status":"public","type":"conference","conference":{"start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France","name":"FOSSACS: Foundations of Software Science and Computation Structures"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"}},{"publisher":"Association for Computing Machinery ","quality_controlled":"1","oa":1,"has_accepted_license":"1","year":"2023","day":"06","publication":"Proceedings of the ACM on Programming Languages","date_published":"2023-06-06T00:00:00Z","doi":"10.1145/3591230","date_created":"2023-07-02T22:00:43Z","article_number":"116","citation":{"mla":"Koval, Nikita, et al. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on Programming Languages, vol. 7, 116, Association for Computing Machinery , 2023, doi:10.1145/3591230.","apa":"Koval, N., Khalanskiy, D., & Alistarh, D.-A. (2023). CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. Association for Computing Machinery . https://doi.org/10.1145/3591230","ama":"Koval N, Khalanskiy D, Alistarh D-A. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 2023;7. doi:10.1145/3591230","ieee":"N. Koval, D. Khalanskiy, and D.-A. Alistarh, “CQS: A formally-verified framework for fair and abortable synchronization,” Proceedings of the ACM on Programming Languages, vol. 7. Association for Computing Machinery , 2023.","short":"N. Koval, D. Khalanskiy, D.-A. Alistarh, Proceedings of the ACM on Programming Languages 7 (2023).","chicago":"Koval, Nikita, Dmitry Khalanskiy, and Dan-Adrian Alistarh. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery , 2023. https://doi.org/10.1145/3591230.","ista":"Koval N, Khalanskiy D, Alistarh D-A. 2023. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 7, 116."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87","first_name":"Nikita","last_name":"Koval","full_name":"Koval, Nikita"},{"first_name":"Dmitry","last_name":"Khalanskiy","full_name":"Khalanskiy, Dmitry"},{"full_name":"Alistarh, Dan-Adrian","orcid":"0000-0003-3650-940X","last_name":"Alistarh","first_name":"Dan-Adrian","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","title":"CQS: A formally-verified framework for fair and abortable synchronization","abstract":[{"text":"Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages—specifically, fair FIFO ordering of synchronization requests and support for abortable operations—and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads.\r\n\r\nThis paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with formal proofs in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java’s AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework’s practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives.","lang":"eng"}],"oa_version":"Published Version","scopus_import":"1","month":"06","intvolume":" 7","publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","file":[{"date_created":"2023-07-03T13:09:39Z","file_name":"2023_ACMProgram.Lang._Koval.pdf","date_updated":"2023-07-03T13:09:39Z","file_size":1266773,"creator":"alisjak","checksum":"5dba6e73f0ed79adbdae14d165bc2f68","file_id":"13187","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"volume":7,"_id":"13179","type":"journal_article","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","date_updated":"2023-07-17T08:43:19Z","ddc":["000"],"department":[{"_id":"DaAl"}],"file_date_updated":"2023-07-03T13:09:39Z"},{"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1944-4184"],"issn":["1944-4176"]},"publication_status":"published","volume":16,"issue":"2","oa_version":"Preprint","abstract":[{"text":"We study the density of everywhere locally soluble diagonal quadric surfaces, parameterised by rational points that lie on a split quadric surface","lang":"eng"}],"month":"05","intvolume":" 16","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2203.06881"}],"date_updated":"2023-07-17T08:39:19Z","department":[{"_id":"TiBr"}],"_id":"13180","status":"public","article_type":"original","type":"journal_article","day":"26","publication":"Involve","year":"2023","date_published":"2023-05-26T00:00:00Z","doi":"10.2140/involve.2023.16.331","date_created":"2023-07-02T22:00:43Z","page":"331-342","publisher":"Mathematical Sciences Publishers","quality_controlled":"1","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Browning, Timothy D., et al. “Local Solubility for a Family of Quadrics over a Split Quadric Surface.” Involve, vol. 16, no. 2, Mathematical Sciences Publishers, 2023, pp. 331–42, doi:10.2140/involve.2023.16.331.","apa":"Browning, T. D., Lyczak, J., & Sarapin, R. (2023). Local solubility for a family of quadrics over a split quadric surface. Involve. Mathematical Sciences Publishers. https://doi.org/10.2140/involve.2023.16.331","ama":"Browning TD, Lyczak J, Sarapin R. Local solubility for a family of quadrics over a split quadric surface. Involve. 2023;16(2):331-342. doi:10.2140/involve.2023.16.331","ieee":"T. D. Browning, J. Lyczak, and R. Sarapin, “Local solubility for a family of quadrics over a split quadric surface,” Involve, vol. 16, no. 2. Mathematical Sciences Publishers, pp. 331–342, 2023.","short":"T.D. Browning, J. Lyczak, R. Sarapin, Involve 16 (2023) 331–342.","chicago":"Browning, Timothy D, Julian Lyczak, and Roman Sarapin. “Local Solubility for a Family of Quadrics over a Split Quadric Surface.” Involve. Mathematical Sciences Publishers, 2023. https://doi.org/10.2140/involve.2023.16.331.","ista":"Browning TD, Lyczak J, Sarapin R. 2023. Local solubility for a family of quadrics over a split quadric surface. Involve. 16(2), 331–342."},"title":"Local solubility for a family of quadrics over a split quadric surface","author":[{"orcid":"0000-0002-8314-0177","full_name":"Browning, Timothy D","last_name":"Browning","id":"35827D50-F248-11E8-B48F-1D18A9856A87","first_name":"Timothy D"},{"first_name":"Julian","id":"3572849A-F248-11E8-B48F-1D18A9856A87","last_name":"Lyczak","full_name":"Lyczak, Julian"},{"full_name":"Sarapin, Roman","last_name":"Sarapin","first_name":"Roman"}],"external_id":{"arxiv":["2203.06881"]},"article_processing_charge":"No"},{"language":[{"iso":"eng"}],"publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","success":1,"file_id":"13250","checksum":"0ab6173cd5c5634ed773cd37ff012681","file_size":380354,"date_updated":"2023-07-18T09:28:30Z","creator":"dernst","file_name":"2023_ASHPC_Elefante.pdf","date_created":"2023-07-18T09:28:30Z"}],"day":"01","publication_status":"accepted","year":"2023","has_accepted_license":"1","date_created":"2023-06-23T11:03:18Z","date_published":"2023-07-01T00:00:00Z","page":"42-42","oa_version":"Submitted Version","month":"07","oa":1,"publisher":"EuroCC","quality_controlled":"1","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-07-18T09:32:16Z","citation":{"mla":"Elefante, Stefano, et al. “Cryo-EM Software Packages: A Sys-Admins Point of View.” ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, pp. 42–42.","ama":"Elefante S, Stadlbauer S, Alexander MF, Schlögl A. Cryo-EM software packages: A sys-admins point of view. In: ASHPC23 - Austrian-Slovenian HPC Meeting 2023. EuroCC; :42-42.","apa":"Elefante, S., Stadlbauer, S., Alexander, M. F., & Schlögl, A. (n.d.). Cryo-EM software packages: A sys-admins point of view. In ASHPC23 - Austrian-Slovenian HPC Meeting 2023 (pp. 42–42). Maribor, Slovenia: EuroCC.","short":"S. Elefante, S. Stadlbauer, M.F. Alexander, A. Schlögl, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 42–42.","ieee":"S. Elefante, S. Stadlbauer, M. F. Alexander, and A. Schlögl, “Cryo-EM software packages: A sys-admins point of view,” in ASHPC23 - Austrian-Slovenian HPC Meeting 2023, Maribor, Slovenia, pp. 42–42.","chicago":"Elefante, Stefano, Stephan Stadlbauer, Michael F Alexander, and Alois Schlögl. “Cryo-EM Software Packages: A Sys-Admins Point of View.” In ASHPC23 - Austrian-Slovenian HPC Meeting 2023, 42–42. EuroCC, n.d.","ista":"Elefante S, Stadlbauer S, Alexander MF, Schlögl A. Cryo-EM software packages: A sys-admins point of view. ASHPC23 - Austrian-Slovenian HPC Meeting 2023. ASHPC: Austrian-Slovenian HPC Meeting, 42–42."},"title":"Cryo-EM software packages: A sys-admins point of view","file_date_updated":"2023-07-18T09:28:30Z","department":[{"_id":"ScienComp"}],"article_processing_charge":"No","author":[{"full_name":"Elefante, Stefano","last_name":"Elefante","first_name":"Stefano","id":"490F40CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Stadlbauer, Stephan","last_name":"Stadlbauer","id":"4D0BC184-F248-11E8-B48F-1D18A9856A87","first_name":"Stephan"},{"id":"3A02A8FA-F248-11E8-B48F-1D18A9856A87","first_name":"Michael F","full_name":"Alexander, Michael F","last_name":"Alexander"},{"last_name":"Schlögl","orcid":"0000-0002-5621-8100","full_name":"Schlögl, Alois","first_name":"Alois","id":"45BF87EE-F248-11E8-B48F-1D18A9856A87"}],"_id":"13162","status":"public","conference":{"start_date":"2023-06-12","location":"Maribor, Slovenia","end_date":"2023-06-15","name":"ASHPC: Austrian-Slovenian HPC Meeting"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference_abstract"},{"publication_status":"inpress","file":[{"success":1,"file_id":"13249","checksum":"ec8e4295d54171032cdd1b01423eb4a6","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2023_ASHPC_Schloegl.pdf","date_created":"2023-07-18T09:18:55Z","creator":"dernst","file_size":316959,"date_updated":"2023-07-18T09:18:55Z"}],"language":[{"iso":"eng"}],"month":"07","oa_version":"Submitted Version","file_date_updated":"2023-07-18T09:18:55Z","department":[{"_id":"ScienComp"},{"_id":"EM-Fac"}],"date_updated":"2023-07-18T09:30:54Z","ddc":["000"],"type":"conference_abstract","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2023-06-13","location":"Maribor, Slovenia","end_date":"2023-06-15","name":"ASHPC: Austrian-Slovenian HPC Meeting"},"status":"public","_id":"13161","page":"59-59","date_published":"2023-07-01T00:00:00Z","date_created":"2023-06-23T11:01:23Z","has_accepted_license":"1","year":"2023","day":"01","publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","publisher":"EuroCC","quality_controlled":"1","oa":1,"acknowledgement":"Thanks to Jesse Hansen for his suggestions on improving the abstract.","author":[{"full_name":"Schlögl, Alois","orcid":"0000-0002-5621-8100","last_name":"Schlögl","first_name":"Alois","id":"45BF87EE-F248-11E8-B48F-1D18A9856A87"},{"id":"490F40CE-F248-11E8-B48F-1D18A9856A87","first_name":"Stefano","last_name":"Elefante","full_name":"Elefante, Stefano"},{"last_name":"Hodirnau","full_name":"Hodirnau, Victor-Valentin","id":"3661B498-F248-11E8-B48F-1D18A9856A87","first_name":"Victor-Valentin"}],"article_processing_charge":"No","title":"Running Windows-applications on a Linux HPC cluster using WINE","citation":{"ista":"Schlögl A, Elefante S, Hodirnau V-V. Running Windows-applications on a Linux HPC cluster using WINE. ASHPC23 - Austrian-Slovenian HPC Meeting 2023. ASHPC: Austrian-Slovenian HPC Meeting, 59–59.","chicago":"Schlögl, Alois, Stefano Elefante, and Victor-Valentin Hodirnau. “Running Windows-Applications on a Linux HPC Cluster Using WINE.” In ASHPC23 - Austrian-Slovenian HPC Meeting 2023, 59–59. EuroCC, n.d.","short":"A. Schlögl, S. Elefante, V.-V. Hodirnau, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 59–59.","ieee":"A. Schlögl, S. Elefante, and V.-V. Hodirnau, “Running Windows-applications on a Linux HPC cluster using WINE,” in ASHPC23 - Austrian-Slovenian HPC Meeting 2023, Maribor, Slovenia, pp. 59–59.","apa":"Schlögl, A., Elefante, S., & Hodirnau, V.-V. (n.d.). Running Windows-applications on a Linux HPC cluster using WINE. In ASHPC23 - Austrian-Slovenian HPC Meeting 2023 (pp. 59–59). Maribor, Slovenia: EuroCC.","ama":"Schlögl A, Elefante S, Hodirnau V-V. Running Windows-applications on a Linux HPC cluster using WINE. In: ASHPC23 - Austrian-Slovenian HPC Meeting 2023. EuroCC; :59-59.","mla":"Schlögl, Alois, et al. “Running Windows-Applications on a Linux HPC Cluster Using WINE.” ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, pp. 59–59."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]