TY - JOUR
AB - We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.
AU - Svoreňová, Mária
AU - Kretinsky, Jan
AU - Chmelik, Martin
AU - Chatterjee, Krishnendu
AU - Cěrná, Ivana
AU - Belta, Cǎlin
ID - 1407
IS - 2
JF - Nonlinear Analysis: Hybrid Systems
TI - Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
VL - 23
ER -
TY - JOUR
AB - Phat is an open-source C. ++ library for the computation of persistent homology by matrix reduction, targeted towards developers of software for topological data analysis. We aim for a simple generic design that decouples algorithms from data structures without sacrificing efficiency or user-friendliness. We provide numerous different reduction strategies as well as data types to store and manipulate the boundary matrix. We compare the different combinations through extensive experimental evaluation and identify optimization techniques that work well in practical situations. We also compare our software with various other publicly available libraries for persistent homology.
AU - Bauer, Ulrich
AU - Kerber, Michael
AU - Reininghaus, Jan
AU - Wagner, Hubert
ID - 1433
JF - Journal of Symbolic Computation
SN - 07477171
TI - Phat - Persistent homology algorithms toolbox
VL - 78
ER -
TY - JOUR
AB - We consider N×N Hermitian random matrices H consisting of blocks of size M≥N6/7. The matrix elements are i.i.d. within the blocks, close to a Gaussian in the four moment matching sense, but their distribution varies from block to block to form a block-band structure, with an essential band width M. We show that the entries of the Green’s function G(z)=(H−z)−1 satisfy the local semicircle law with spectral parameter z=E+iη down to the real axis for any η≫N−1, using a combination of the supersymmetry method inspired by Shcherbina (J Stat Phys 155(3): 466–499, 2014) and the Green’s function comparison strategy. Previous estimates were valid only for η≫M−1. The new estimate also implies that the eigenvectors in the middle of the spectrum are fully delocalized.
AU - Bao, Zhigang
AU - Erdös, László
ID - 1528
IS - 3-4
JF - Probability Theory and Related Fields
SN - 01788051
TI - Delocalization for a class of random block band matrices
VL - 167
ER -
TY - CONF
AB - We study probabilistic models of natural images and extend the autoregressive family of PixelCNN models by incorporating latent variables. Subsequently, we describe two new generative image models that exploit different image transformations as latent variables: a quantized grayscale view of the image or a multi-resolution image pyramid. The proposed models tackle two known shortcomings of existing PixelCNN models: 1) their tendency to focus on low-level image details, while largely ignoring high-level image information, such as object shapes, and 2) their computationally costly procedure for image sampling. We experimentally demonstrate benefits of our LatentPixelCNN models, in particular showing that they produce much more realistically looking image samples than previous state-of-the-art probabilistic models.
AU - Kolesnikov, Alexander
AU - Lampert, Christoph
ID - 1000
SN - 978-151085514-4
TI - PixelCNN models with auxiliary variables for natural image modeling
VL - 70
ER -
TY - CONF
AB - We present a computational approach for designing CurveUps, curvy shells that form from an initially flat state. They consist of small rigid tiles that are tightly held together by two pre-stretched elastic sheets attached to them. Our method allows the realization of smooth, doubly curved surfaces that can be fabricated as a flat piece. Once released, the restoring forces of the pre-stretched sheets support the object to take shape in 3D. CurveUps are structurally stable in their target configuration. The design process starts with a target surface. Our method generates a tile layout in 2D and optimizes the distribution, shape, and attachment areas of the tiles to obtain a configuration that is fabricable and in which the curved up state closely matches the target. Our approach is based on an efficient approximate model and a local optimization strategy for an otherwise intractable nonlinear optimization problem. We demonstrate the effectiveness of our approach for a wide range of shapes, all realized as physical prototypes.
AU - Guseinov, Ruslan
AU - Miguel, Eder
AU - Bickel, Bernd
ID - 1001
IS - 4
TI - CurveUps: Shaping objects from flat plates with tension-actuated curvature
VL - 36
ER -