TY - CONF AB - 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. AU - Chatterjee, Krishnendu AU - Henzinger, Thomas A AU - Lechner, Mathias AU - Zikelic, Dorde ID - 13142 SN - 0302-9743 T2 - Tools and Algorithms for the Construction and Analysis of Systems TI - A learner-verifier framework for neural network controllers and certificates of stochastic systems VL - 13993 ER - TY - CONF AB - 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) Ψ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness). For 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 ω -regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive. AU - Anand, Ashwani AU - Mallik, Kaushik AU - Nayak, Satya Prakash AU - Schmuck, Anne Kathrin ID - 13141 SN - 0302-9743 T2 - TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems TI - Computing adequately permissive assumptions for synthesis VL - 13994 ER - TY - THES AB - 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. Firstly, 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. Secondly, 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. Taken 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. AU - Pokusaeva, Victoria ID - 12826 SN - 2663 - 337X TI - Neural control of optic flow-based navigation in Drosophila melanogaster ER - TY - JOUR AB - 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. AU - Edelsbrunner, Herbert AU - Osang, Georg F ID - 12086 JF - Algorithmica SN - 0178-4617 TI - A simple algorithm for higher-order Delaunay mosaics and alpha shapes VL - 85 ER - TY - JOUR AB - 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. AU - Dello Schiavo, Lorenzo AU - Wirth, Melchior ID - 12104 IS - 1 JF - Journal of Evolution Equations SN - 1424-3199 TI - Ergodic decompositions of Dirichlet forms under order isomorphisms VL - 23 ER -