@phdthesis{14711, abstract = {In nature, different species find their niche in a range of environments, each with its unique characteristics. While some thrive in uniform (homogeneous) landscapes where environmental conditions stay relatively consistent across space, others traverse the complexities of spatially heterogeneous terrains. Comprehending how species are distributed and how they interact within these landscapes holds the key to gaining insights into their evolutionary dynamics while also informing conservation and management strategies. For species inhabiting heterogeneous landscapes, when the rate of dispersal is low compared to spatial fluctuations in selection pressure, localized adaptations may emerge. Such adaptation in response to varying selection strengths plays an important role in the persistence of populations in our rapidly changing world. Hence, species in nature are continuously in a struggle to adapt to local environmental conditions, to ensure their continued survival. Natural populations can often adapt in time scales short enough for evolutionary changes to influence ecological dynamics and vice versa, thereby creating a feedback between evolution and demography. The analysis of this feedback and the relative contributions of gene flow, demography, drift, and natural selection to genetic variation and differentiation has remained a recurring theme in evolutionary biology. Nevertheless, the effective role of these forces in maintaining variation and shaping patterns of diversity is not fully understood. Even in homogeneous environments devoid of local adaptations, such understanding remains elusive. Understanding this feedback is crucial, for example in determining the conditions under which extinction risk can be mitigated in peripheral populations subject to deleterious mutation accumulation at the edges of species’ ranges as well as in highly fragmented populations. In this thesis we explore both uniform and spatially heterogeneous metapopulations, investigating and providing theoretical insights into the dynamics of local adaptation in the latter and examining the dynamics of load and extinction as well as the impact of joint ecological and evolutionary (eco-evolutionary) dynamics in the former. The thesis is divided into 5 chapters. Chapter 1 provides a general introduction into the subject matter, clarifying concepts and ideas used throughout the thesis. In chapter 2, we explore how fast a species distributed across a heterogeneous landscape adapts to changing conditions marked by alterations in carrying capacity, selection pressure, and migration rate. In chapter 3, we investigate how migration selection and drift influences adaptation and the maintenance of variation in a metapopulation with three habitats, an extension of previous models of adaptation in two habitats. We further develop analytical approximations for the critical threshold required for polymorphism to persist. The focus of chapter 4 of the thesis is on understanding the interplay between ecology and evolution as coupled processes. We investigate how eco-evolutionary feedback between migration, selection, drift, and demography influences eco-evolutionary outcomes in marginal populations subject to deleterious mutation accumulation. Using simulations as well as theoretical approximations of the coupled dynamics of population size and allele frequency, we analyze how gene flow from a large mainland source influences genetic load and population size on an island (i.e., in a marginal population) under genetically realistic assumptions. Analyses of this sort are important because small isolated populations, are repeatedly affected by complex interactions between ecological and evolutionary processes, which can lead to their death. Understanding these interactions can therefore provide an insight into the conditions under which extinction risk can be mitigated in peripheral populations thus, contributing to conservation and restoration efforts. Chapter 5 extends the analysis in chapter 4 to consider the dynamics of load (due to deleterious mutation accumulation) and extinction risk in a metapopulation. We explore the role of gene flow, selection, and dominance on load and extinction risk and further pinpoint critical thresholds required for metapopulation persistence. Overall this research contributes to our understanding of ecological and evolutionary mechanisms that shape species’ persistence in fragmented landscapes, a crucial foundation for successful conservation efforts and biodiversity management.}, author = {Olusanya, Oluwafunmilola O}, issn = {2663 - 337X}, pages = {183}, publisher = {Institute of Science and Technology Austria}, title = {{Local adaptation, genetic load and extinction in metapopulations}}, doi = {10.15479/at:ista:14711}, year = {2024}, } @phdthesis{14821, author = {Chiossi, Heloisa}, issn = {2663 - 337X}, pages = {89}, publisher = {Institute of Science and Technology Austria}, title = {{Adaptive hierarchical representations in the hippocampus}}, doi = {10.15479/at:ista:14821}, year = {2024}, } @phdthesis{15020, abstract = {This thesis consists of four distinct pieces of work within theoretical biology, with two themes in common: the concept of optimization in biological systems, and the use of information-theoretic tools to quantify biological stochasticity and statistical uncertainty. Chapter 2 develops a statistical framework for studying biological systems which we believe to be optimized for a particular utility function, such as retinal neurons conveying information about visual stimuli. We formalize such beliefs as maximum-entropy Bayesian priors, constrained by the expected utility. We explore how such priors aid inference of system parameters with limited data and enable optimality hypothesis testing: is the utility higher than by chance? Chapter 3 examines the ultimate biological optimization process: evolution by natural selection. As some individuals survive and reproduce more successfully than others, populations evolve towards fitter genotypes and phenotypes. We formalize this as accumulation of genetic information, and use population genetics theory to study how much such information can be accumulated per generation and maintained in the face of random mutation and genetic drift. We identify the population size and fitness variance as the key quantities that control information accumulation and maintenance. Chapter 4 reuses the concept of genetic information from Chapter 3, but from a different perspective: we ask how much genetic information organisms actually need, in particular in the context of gene regulation. For example, how much information is needed to bind transcription factors at correct locations within the genome? Population genetics provides us with a refined answer: with an increasing population size, populations achieve higher fitness by maintaining more genetic information. Moreover, regulatory parameters experience selection pressure to optimize the fitness-information trade-off, i.e. minimize the information needed for a given fitness. This provides an evolutionary derivation of the optimization priors introduced in Chapter 2. Chapter 5 proves an upper bound on mutual information between a signal and a communication channel output (such as neural activity). Mutual information is an important utility measure for biological systems, but its practical use can be difficult due to the large dimensionality of many biological channels. Sometimes, a lower bound on mutual information is computed by replacing the high-dimensional channel outputs with decodes (signal estimates). Our result provides a corresponding upper bound, provided that the decodes are the maximum posterior estimates of the signal.}, author = {Hledik, Michal}, issn = {2663 - 337X}, keywords = {Theoretical biology, Optimality, Evolution, Information}, pages = {158}, publisher = {Institute of Science and Technology Austria}, title = {{Genetic information and biological optimization}}, doi = {10.15479/at:ista:15020}, year = {2024}, } @inproceedings{14317, abstract = {Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization. In light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.}, author = {Akshay, S. and Chatterjee, Krishnendu and Meggendorfer, Tobias and Zikelic, Dorde}, booktitle = {International Conference on Computer Aided Verification}, isbn = {9783031377082}, issn = {1611-3349}, location = {Paris, France}, pages = {86--112}, publisher = {Springer Nature}, title = {{MDPs as distribution transformers: Affine invariant synthesis for safety objectives}}, doi = {10.1007/978-3-031-37709-9_5}, volume = {13966}, year = {2023}, } @phdthesis{14506, abstract = {Payment channel networks are a promising approach to improve the scalability bottleneck of cryptocurrencies. Two design principles behind payment channel networks are efficiency and privacy. Payment channel networks improve efficiency by allowing users to transact in a peer-to-peer fashion along multi-hop routes in the network, avoiding the lengthy process of consensus on the blockchain. Transacting over payment channel networks also improves privacy as these transactions are not broadcast to the blockchain. Despite the influx of recent protocols built on top of payment channel networks and their analysis, a common shortcoming of many of these protocols is that they typically focus only on either improving efficiency or privacy, but not both. Another limitation on the efficiency front is that the models used to model actions, costs and utilities of users are limited or come with unrealistic assumptions. This thesis aims to address some of the shortcomings of recent protocols and algorithms on payment channel networks, particularly in their privacy and efficiency aspects. We first present a payment route discovery protocol based on hub labelling and private information retrieval that hides the route query and is also efficient. We then present a rebalancing protocol that formulates the rebalancing problem as a linear program and solves the linear program using multiparty computation so as to hide the channel balances. The rebalancing solution as output by our protocol is also globally optimal. We go on to develop more realistic models of the action space, costs, and utilities of both existing and new users that want to join the network. In each of these settings, we also develop algorithms to optimise the utility of these users with good guarantees on the approximation and competitive ratios.}, author = {Yeo, Michelle X}, issn = {2663 - 337X}, pages = {162}, publisher = {Institute of Science and Technology Austria}, title = {{Advances in efficiency and privacy in payment channel network analysis}}, doi = {10.15479/14506}, year = {2023}, } @phdthesis{14510, author = {Gnyliukh, Nataliia}, isbn = {978-3-99078-037-4}, issn = {2663-337X}, keywords = {Clathrin-Mediated Endocytosis, vesicle scission, Dynamin-Related Protein 2, SH3P2, TPLATE complex, Total internal reflection fluorescence microscopy, Arabidopsis thaliana}, pages = {180}, publisher = {Institute of Science and Technology Austria}, title = {{Mechanism of clathrin-coated vesicle formation during endocytosis in plants}}, doi = {10.15479/at:ista:14510}, year = {2023}, } @inproceedings{14518, abstract = {We consider bidding games, a class of two-player zero-sum graph games. The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of a graph, in each turn the players simultaneously submit bids, and the higher bidder moves the token, where we break bidding ties in favor of Player 1. Player 1 wins the game iff the token visits a designated target vertex. We consider, for the first time, poorman discrete-bidding in which the granularity of the bids is restricted and the higher bid is paid to the bank. Previous work either did not impose granularity restrictions or considered Richman bidding (bids are paid to the opponent). While the latter mechanisms are technically more accessible, the former is more appealing from a practical standpoint. Our study focuses on threshold budgets, which is the necessary and sufficient initial budget required for Player 1 to ensure winning against a given Player 2 budget. We first show existence of thresholds. In DAGs, we show that threshold budgets can be approximated with error bounds by thresholds under continuous-bidding and that they exhibit a periodic behavior. We identify closed-form solutions in special cases. We implement and experiment with an algorithm to find threshold budgets.}, author = {Avni, Guy and Meggendorfer, Tobias and Sadhukhan, Suman and Tkadlec, Josef and Zikelic, Dorde}, booktitle = {Frontiers in Artificial Intelligence and Applications}, isbn = {9781643684369}, issn = {0922-6389}, location = {Krakow, Poland}, pages = {141--148}, publisher = {IOS Press}, title = {{Reachability poorman discrete-bidding games}}, doi = {10.3233/FAIA230264}, volume = {372}, year = {2023}, } @phdthesis{14539, abstract = {Stochastic systems provide a formal framework for modelling and quantifying uncertainty in systems and have been widely adopted in many application domains. Formal verification and control of finite state stochastic systems, a subfield of formal methods also known as probabilistic model checking, is well studied. In contrast, formal verification and control of infinite state stochastic systems have received comparatively less attention. However, infinite state stochastic systems commonly arise in practice. For instance, probabilistic models that contain continuous probability distributions such as normal or uniform, or stochastic dynamical systems which are a classical model for control under uncertainty, both give rise to infinite state systems. The goal of this thesis is to contribute to laying theoretical and algorithmic foundations of fully automated formal verification and control of infinite state stochastic systems, with a particular focus on systems that may be executed over a long or infinite time. We consider formal verification of infinite state stochastic systems in the setting of static analysis of probabilistic programs and formal control in the setting of controller synthesis in stochastic dynamical systems. For both problems, we present some of the first fully automated methods for probabilistic (a.k.a. quantitative) reachability and safety analysis applicable to infinite time horizon systems. We also advance the state of the art of probability 1 (a.k.a. qualitative) reachability analysis for both problems. Finally, for formal controller synthesis in stochastic dynamical systems, we present a novel framework for learning neural network control policies in stochastic dynamical systems with formal guarantees on correctness with respect to quantitative reachability, safety or reach-avoid specifications. }, author = {Zikelic, Dorde}, isbn = {978-3-99078-036-7}, issn = {2663 - 337X}, pages = {256}, publisher = {Institute of Science and Technology Austria}, title = {{Automated verification and control of infinite state stochastic systems}}, doi = {10.15479/14539}, year = {2023}, } @inproceedings{14559, abstract = {We consider the problem of learning control policies in discrete-time stochastic systems which guarantee that the system stabilizes within some specified stabilization region with probability 1. Our approach is based on the novel notion of stabilizing ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome the limitation of methods proposed in previous works whose applicability is restricted to systems in which the stabilizing region cannot be left once entered under any control policy. We present a learning procedure that learns a control policy together with an sRSM that formally certifies probability 1 stability, both learned as neural networks. We show that this procedure can also be adapted to formally verifying that, under a given Lipschitz continuous control policy, the stochastic system stabilizes within some stabilizing region with probability 1. Our experimental evaluation shows that our learning procedure can successfully learn provably stabilizing policies in practice.}, author = {Ansaripour, Matin and Chatterjee, Krishnendu and Henzinger, Thomas A and Lechner, Mathias and Zikelic, Dorde}, booktitle = {21st International Symposium on Automated Technology for Verification and Analysis}, isbn = {9783031453281}, issn = {1611-3349}, location = {Singapore, Singapore}, pages = {357--379}, publisher = {Springer Nature}, title = {{Learning provably stabilizing neural controllers for discrete-time stochastic systems}}, doi = {10.1007/978-3-031-45329-8_17}, volume = {14215}, year = {2023}, } @unpublished{14591, abstract = {Clathrin-mediated endocytosis (CME) is vital for the regulation of plant growth and development by controlling plasma membrane protein composition and cargo uptake. CME relies on the precise recruitment of regulators for vesicle maturation and release. Homologues of components of mammalian vesicle scission are strong candidates to be part of the scissin machinery in plants, but the precise roles of these proteins in this process is not fully understood. Here, we characterised the roles of Plant Dynamin-Related Proteins 2 (DRP2s) and SH3-domain containing protein 2 (SH3P2), the plant homologue to Dynamins’ recruiters, like Endophilin and Amphiphysin, in the CME by combining high-resolution imaging of endocytic events in vivo and characterisation of the purified proteins in vitro. Although DRP2s and SH3P2 arrive similarly late during CME and physically interact, genetic analysis of the Dsh3p1,2,3 triple-mutant and complementation assays with non-SH3P2-interacting DRP2 variants suggests that SH3P2 does not directly recruit DRP2s to the site of endocytosis. These observations imply that despite the presence of many well-conserved endocytic components, plants have acquired a distinct mechanism for CME. One Sentence Summary In contrast to predictions based on mammalian systems, plant Dynamin-related proteins 2 are recruited to the site of Clathrin-mediated endocytosis independently of BAR-SH3 proteins.}, author = {Gnyliukh, Nataliia and Johnson, Alexander J and Nagel, Marie-Kristin and Monzer, Aline and Hlavata, Annamaria and Isono, Erika and Loose, Martin and Friml, Jiří}, booktitle = {bioRxiv}, title = {{Role of dynamin-related proteins 2 and SH3P2 in clathrin-mediated endocytosis in plants}}, doi = {10.1101/2023.10.09.561523}, year = {2023}, } @phdthesis{14641, author = {Hennessey-Wesen, Mike}, issn = {2663 - 337X}, keywords = {microfluidics, miceobiology, mutations, quorum sensing}, pages = {104}, publisher = {Institute of Science and Technology Austria}, title = {{Adaptive mutation in E. coli modulated by luxS}}, doi = {10.15479/at:ista:14641}, year = {2023}, } @phdthesis{14651, abstract = {For self-incompatibility (SI) to be stable in a population, theory predicts that sufficient inbreeding depression (ID) is required: the fitness of offspring from self-mated individuals must be low enough to prevent the spread of self-compatibility (SC). Reviews of natural plant populations have supported this theory, with SI species generally showing high levels of ID. However, there is thought to be an under-sampling of self-incompatible taxa in the current literature. In this thesis, I study inbreeding depression in the SI plant species Antirrhinum majus using both greenhouse crosses and a large collected field dataset. Additionally, the gametophytic S-locus of A. majus is highly heterozygous and polymorphic, thus making assembly and discovery of S-alleles very difficult. Here, 206 new alleles of the male component SLFs are presented, along with a phylogeny showing the high conservation with alleles from another Antirrhinum species. Lastly, selected sites within the protein structure of SLFs are investigated, with one site in particular highlighted as potentially being involved in the SI recognition mechanism.}, author = {Arathoon, Louise S}, issn = {2663 - 337X}, pages = {96}, publisher = {Institute of Science and Technology Austria}, title = {{Investigating inbreeding depression and the self-incompatibility locus of Antirrhinum majus}}, doi = {10.15479/at:ista:14651}, year = {2023}, } @article{14656, abstract = {Although much is known about how single neurons in the hippocampus represent an animal's position, how circuit interactions contribute to spatial coding is less well understood. Using a novel statistical estimator and theoretical modeling, both developed in the framework of maximum entropy models, we reveal highly structured CA1 cell-cell interactions in male rats during open field exploration. The statistics of these interactions depend on whether the animal is in a familiar or novel environment. In both conditions the circuit interactions optimize the encoding of spatial information, but for regimes that differ in the informativeness of their spatial inputs. This structure facilitates linear decodability, making the information easy to read out by downstream circuits. Overall, our findings suggest that the efficient coding hypothesis is not only applicable to individual neuron properties in the sensory periphery, but also to neural interactions in the central brain.}, author = {Nardin, Michele and Csicsvari, Jozsef L and Tkačik, Gašper and Savin, Cristina}, issn = {1529-2401}, journal = {The Journal of Neuroscience}, number = {48}, pages = {8140--8156}, publisher = {Society of Neuroscience}, title = {{The structure of hippocampal CA1 interactions optimizes spatial coding across experience}}, doi = {10.1523/JNEUROSCI.0194-23.2023}, volume = {43}, year = {2023}, } @phdthesis{14697, author = {Stopp, Julian A}, isbn = {978-3-99078-038-1}, issn = {2663 - 337X}, pages = {226}, publisher = {Institute of Science and Technology Austria}, title = {{Neutrophils on the hunt: Migratory strategies employed by neutrophils to fulfill their effector function}}, doi = {10.15479/at:ista:14697}, year = {2023}, } @article{14778, abstract = {We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshady, Ehsan and Novotný, Petr and Zárevúcky, Jiří and Zikelic, Dorde}, issn = {1433-299X}, journal = {Formal Aspects of Computing}, keywords = {Theoretical Computer Science, Software}, number = {2}, publisher = {Association for Computing Machinery}, title = {{On lexicographic proof rules for probabilistic termination}}, doi = {10.1145/3585391}, volume = {35}, year = {2023}, } @inproceedings{14830, abstract = {We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.}, author = {Zikelic, Dorde and Lechner, Mathias and Henzinger, Thomas A and Chatterjee, Krishnendu}, booktitle = {Proceedings of the 37th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, keywords = {General Medicine}, location = {Washington, DC, United States}, number = {10}, pages = {11926--11935}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Learning control policies for stochastic systems with reach-avoid guarantees}}, doi = {10.1609/aaai.v37i10.26407}, volume = {37}, year = {2023}, } @phdthesis{13074, abstract = {Deep learning has become an integral part of a large number of important applications, and many of the recent breakthroughs have been enabled by the ability to train very large models, capable to capture complex patterns and relationships from the data. At the same time, the massive sizes of modern deep learning models have made their deployment to smaller devices more challenging; this is particularly important, as in many applications the users rely on accurate deep learning predictions, but they only have access to devices with limited memory and compute power. One solution to this problem is to prune neural networks, by setting as many of their parameters as possible to zero, to obtain accurate sparse models with lower memory footprint. Despite the great research progress in obtaining sparse models that preserve accuracy, while satisfying memory and computational constraints, there are still many challenges associated with efficiently training sparse models, as well as understanding their generalization properties. The focus of this thesis is to investigate how the training process of sparse models can be made more efficient, and to understand the differences between sparse and dense models in terms of how well they can generalize to changes in the data distribution. We first study a method for co-training sparse and dense models, at a lower cost compared to regular training. With our method we can obtain very accurate sparse networks, and dense models that can recover the baseline accuracy. Furthermore, we are able to more easily analyze the differences, at prediction level, between the sparse-dense model pairs. Next, we investigate the generalization properties of sparse neural networks in more detail, by studying how well different sparse models trained on a larger task can adapt to smaller, more specialized tasks, in a transfer learning scenario. Our analysis across multiple pruning methods and sparsity levels reveals that sparse models provide features that can transfer similarly to or better than the dense baseline. However, the choice of the pruning method plays an important role, and can influence the results when the features are fixed (linear finetuning), or when they are allowed to adapt to the new task (full finetuning). Using sparse models with fixed masks for finetuning on new tasks has an important practical advantage, as it enables training neural networks on smaller devices. However, one drawback of current pruning methods is that the entire training cycle has to be repeated to obtain the initial sparse model, for every sparsity target; in consequence, the entire training process is costly and also multiple models need to be stored. In the last part of the thesis we propose a method that can train accurate dense models that are compressible in a single step, to multiple sparsity levels, without additional finetuning. Our method results in sparse models that can be competitive with existing pruning methods, and which can also successfully generalize to new tasks.}, author = {Peste, Elena-Alexandra}, issn = {2663-337X}, pages = {147}, publisher = {Institute of Science and Technology Austria}, title = {{Efficiency and generalization of sparse neural networks}}, doi = {10.15479/at:ista:13074}, year = {2023}, } @misc{13126, abstract = {Mapping the complex and dense arrangement of cells and their connectivity in brain tissue demands nanoscale spatial resolution imaging. Super-resolution optical microscopy excels at visualizing specific molecules and individual cells but fails to provide tissue context. Here, we developed Comprehensive Analysis of Tissues across Scales (CATS), a technology to densely map brain tissue architecture from millimeter regional to nanometer synaptic scales in diverse chemically fixed brain preparations, including rodent and human. CATS uses fixation-compatible extracellular labeling and optical imaging, including stimulated emission depletion or expansion microscopy, to comprehensively delineate cellular structures. It enables three-dimensional reconstruction of single synapses and mapping of synaptic connectivity by identification and analysis of putative synaptic cleft regions. Applying CATS to the mouse hippocampal mossy fiber circuitry, we reconstructed and quantified the synaptic input and output structure of identified neurons. We furthermore demonstrate applicability to clinically derived human tissue samples, including formalin-fixed paraffin-embedded routine diagnostic specimens, for visualizing the cellular architecture of brain tissue in health and disease.}, author = {Danzl, Johann G}, publisher = {Institute of Science and Technology Austria}, title = {{Research data for the publication "Imaging brain tissue architecture across millimeter to nanometer scales"}}, doi = {10.15479/AT:ISTA:13126}, year = {2023}, } @inproceedings{13142, abstract = {Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Lechner, Mathias and Zikelic, Dorde}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems }, isbn = {9783031308222}, issn = {1611-3349}, location = {Paris, France}, pages = {3--25}, publisher = {Springer Nature}, title = {{A learner-verifier framework for neural network controllers and certificates of stochastic systems}}, doi = {10.1007/978-3-031-30823-9_1}, volume = {13993}, year = {2023}, } @article{13267, abstract = {Three-dimensional (3D) reconstruction of living brain tissue down to an individual synapse level would create opportunities for decoding the dynamics and structure–function relationships of the brain’s complex and dense information processing network; however, this has been hindered by insufficient 3D resolution, inadequate signal-to-noise ratio and prohibitive light burden in optical imaging, whereas electron microscopy is inherently static. Here we solved these challenges by developing an integrated optical/machine-learning technology, LIONESS (live information-optimized nanoscopy enabling saturated segmentation). This leverages optical modifications to stimulated emission depletion microscopy in comprehensively, extracellularly labeled tissue and previous information on sample structure via machine learning to simultaneously achieve isotropic super-resolution, high signal-to-noise ratio and compatibility with living tissue. This allows dense deep-learning-based instance segmentation and 3D reconstruction at a synapse level, incorporating molecular, activity and morphodynamic information. LIONESS opens up avenues for studying the dynamic functional (nano-)architecture of living brain tissue.}, author = {Velicky, Philipp and Miguel Villalba, Eder and Michalska, Julia M and Lyudchik, Julia and Wei, Donglai and Lin, Zudi and Watson, Jake and Troidl, Jakob and Beyer, Johanna and Ben Simon, Yoav and Sommer, Christoph M and Jahr, Wiebke and Cenameri, Alban and Broichhagen, Johannes and Grant, Seth G.N. and Jonas, Peter M and Novarino, Gaia and Pfister, Hanspeter and Bickel, Bernd and Danzl, Johann G}, issn = {1548-7105}, journal = {Nature Methods}, pages = {1256--1265}, publisher = {Springer Nature}, title = {{Dense 4D nanoscale reconstruction of living brain tissue}}, doi = {10.1038/s41592-023-01936-6}, volume = {20}, year = {2023}, }