TY - CONF
AB - In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.
AU - Nguyen, Luan
AU - Schilling, Christian
AU - Bogomolov, Sergiy
AU - Johnson, Taylor
ID - 1606
TI - Runtime verification for hybrid analysis tools
VL - 9333
ER -
TY - CONF
AB - The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is “constructed from scratch” rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.
AU - Chatterjee, Krishnendu
AU - Doyen, Laurent
AU - Vardi, Moshe
ID - 1609
TI - The complexity of synthesis from probabilistic components
VL - 9135
ER -
TY - CONF
AB - The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Ibsen-Jensen, Rasmus
AU - Otop, Jan
ID - 1610
IS - Part II
TI - Edit distance for pushdown automata
VL - 9135
ER -
TY - JOUR
AB - Biosensors for signaling molecules allow the study of physiological processes by bringing together the fields of protein engineering, fluorescence imaging, and cell biology. Construction of genetically encoded biosensors generally relies on the availability of a binding "core" that is both specific and stable, which can then be combined with fluorescent molecules to create a sensor. However, binding proteins with the desired properties are often not available in nature and substantial improvement to sensors can be required, particularly with regard to their durability. Ancestral protein reconstruction is a powerful protein-engineering tool able to generate highly stable and functional proteins. In this work, we sought to establish the utility of ancestral protein reconstruction to biosensor development, beginning with the construction of an l-arginine biosensor. l-arginine, as the immediate precursor to nitric oxide, is an important molecule in many physiological contexts including brain function. Using a combination of ancestral reconstruction and circular permutation, we constructed a Förster resonance energy transfer (FRET) biosensor for l-arginine (cpFLIPR). cpFLIPR displays high sensitivity and specificity, with a Kd of ∼14 μM and a maximal dynamic range of 35%. Importantly, cpFLIPR was highly robust, enabling accurate l-arginine measurement at physiological temperatures. We established that cpFLIPR is compatible with two-photon excitation fluorescence microscopy and report l-arginine concentrations in brain tissue.
AU - Whitfield, Jason
AU - Zhang, William
AU - Herde, Michel
AU - Clifton, Ben
AU - Radziejewski, Johanna
AU - Janovjak, Harald L
AU - Henneberger, Christian
AU - Jackson, Colin
ID - 1611
IS - 9
JF - Protein Science
TI - Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction
VL - 24
ER -
TY - JOUR
AB - GABAergic perisoma-inhibiting fast-spiking interneurons (PIIs) effectively control the activity of large neuron populations by their wide axonal arborizations. It is generally assumed that the output of one PII to its target cells is strong and rapid. Here, we show that, unexpectedly, both strength and time course of PII-mediated perisomatic inhibition change with distance between synaptically connected partners in the rodent hippocampus. Synaptic signals become weaker due to lower contact numbers and decay more slowly with distance, very likely resulting from changes in GABAA receptor subunit composition. When distance-dependent synaptic inhibition is introduced to a rhythmically active neuronal network model, randomly driven principal cell assemblies are strongly synchronized by the PIIs, leading to higher precision in principal cell spike times than in a network with uniform synaptic inhibition.
AU - Strüber, Michael
AU - Jonas, Peter M
AU - Bartos, Marlene
ID - 1614
IS - 4
JF - PNAS
TI - Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells
VL - 112
ER -
TY - JOUR
AB - Loss-of-function mutations in the synaptic adhesion protein Neuroligin-4 are among the most common genetic abnormalities associated with autism spectrum disorders, but little is known about the function of Neuroligin-4 and the consequences of its loss. We assessed synaptic and network characteristics in Neuroligin-4 knockout mice, focusing on the hippocampus as a model brain region with a critical role in cognition and memory, and found that Neuroligin-4 deletion causes subtle defects of the protein composition and function of GABAergic synapses in the hippocampal CA3 region. Interestingly, these subtle synaptic changes are accompanied by pronounced perturbations of γ-oscillatory network activity, which has been implicated in cognitive function and is altered in multiple psychiatric and neurodevelopmental disorders. Our data provide important insights into the mechanisms by which Neuroligin-4-dependent GABAergic synapses may contribute to autism phenotypes and indicate new strategies for therapeutic approaches.
AU - Hammer, Matthieu
AU - Krueger Burg, Dilja
AU - Tuffy, Liam
AU - Cooper, Benjamin
AU - Taschenberger, Holger
AU - Goswami, Sarit
AU - Ehrenreich, Hannelore
AU - Jonas, Peter M
AU - Varoqueaux, Frederique
AU - Rhee, Jeong
AU - Brose, Nils
ID - 1615
IS - 3
JF - Cell Reports
TI - Perturbed hippocampal synaptic inhibition and γ-oscillations in a neuroligin-4 knockout mouse model of autism
VL - 13
ER -
TY - JOUR
AB - CCL19 and CCL21 are chemokines involved in the trafficking of immune cells, particularly within the lymphatic system, through activation of CCR7. Concurrent expression of PSGL-1 and CCR7 in naive T-cells enhances recruitment of these cells to secondary lymphoid organs by CCL19 and CCL21. Here the solution structure of CCL19 is reported. It contains a canonical chemokine domain. Chemical shift mapping shows the N-termini of PSGL-1 and CCR7 have overlapping binding sites for CCL19 and binding is competitive. Implications for the mechanism of PSGL-1's enhancement of resting T-cell recruitment are discussed.
AU - Veldkamp, Christopher
AU - Kiermaier, Eva
AU - Gabel Eissens, Skylar
AU - Gillitzer, Miranda
AU - Lippner, David
AU - Disilvio, Frank
AU - Mueller, Casey
AU - Wantuch, Paeton
AU - Chaffee, Gary
AU - Famiglietti, Michael
AU - Zgoba, Danielle
AU - Bailey, Asha
AU - Bah, Yaya
AU - Engebretson, Samantha
AU - Graupner, David
AU - Lackner, Emily
AU - Larosa, Vincent
AU - Medeiros, Tysha
AU - Olson, Michael
AU - Phillips, Andrew
AU - Pyles, Harley
AU - Richard, Amanda
AU - Schoeller, Scott
AU - Touzeau, Boris
AU - Williams, Larry
AU - Sixt, Michael K
AU - Peterson, Francis
ID - 1618
IS - 27
JF - Biochemistry
TI - Solution structure of CCL19 and identification of overlapping CCR7 and PSGL-1 binding sites
VL - 54
ER -
TY - JOUR
AB - Background
Photosynthetic cyanobacteria are attractive for a range of biotechnological applications including biofuel production. However, due to slow growth, screening of mutant libraries using microtiter plates is not feasible.
Results
We present a method for high-throughput, single-cell analysis and sorting of genetically engineered l-lactate-producing strains of Synechocystis sp. PCC6803. A microfluidic device is used to encapsulate single cells in picoliter droplets, assay the droplets for l-lactate production, and sort strains with high productivity. We demonstrate the separation of low- and high-producing reference strains, as well as enrichment of a more productive l-lactate-synthesizing population after UV-induced mutagenesis. The droplet platform also revealed population heterogeneity in photosynthetic growth and lactate production, as well as the presence of metabolically stalled cells.
Conclusions
The workflow will facilitate metabolic engineering and directed evolution studies and will be useful in studies of cyanobacteria biochemistry and physiology.
AU - Hammar, Petter
AU - Angermayr, Andreas
AU - Sjostrom, Staffan
AU - Van Der Meer, Josefin
AU - Hellingwerf, Klaas
AU - Hudson, Elton
AU - Joensson, Hakaan
ID - 1623
IS - 1
JF - Biotechnology for Biofuels
TI - Single-cell screening of photosynthetic growth and lactate production by cyanobacteria
VL - 8
ER -
TY - JOUR
AB - Population structure can facilitate evolution of cooperation. In a structured population, cooperators can form clusters which resist exploitation by defectors. Recently, it was observed that a shift update rule is an extremely strong amplifier of cooperation in a one dimensional spatial model. For the shift update rule, an individual is chosen for reproduction proportional to fecundity; the offspring is placed next to the parent; a random individual dies. Subsequently, the population is rearranged (shifted) until all individual cells are again evenly spaced out. For large population size and a one dimensional population structure, the shift update rule favors cooperation for any benefit-to-cost ratio greater than one. But every attempt to generalize shift updating to higher dimensions while maintaining its strong effect has failed. The reason is that in two dimensions the clusters are fragmented by the movements caused by rearranging the cells. Here we introduce the natural phenomenon of a repulsive force between cells of different types. After a birth and death event, the cells are being rearranged minimizing the overall energy expenditure. If the repulsive force is sufficiently high, shift becomes a strong promoter of cooperation in two dimensions.
AU - Pavlogiannis, Andreas
AU - Chatterjee, Krishnendu
AU - Adlam, Ben
AU - Nowak, Martin
ID - 1624
JF - Scientific Reports
TI - Cellular cooperation with shift updating and repulsion
VL - 5
ER -
TY - CONF
AB - In recent years we have seen numerous improvements on 3D scanning and tracking of human faces, greatly advancing the creation of digital doubles for film and video games. However, despite the high-resolution quality of the reconstruction approaches available, current methods are unable to capture one of the most important regions of the face - the eye region. In this work we present the first method for detailed spatio-temporal reconstruction of eyelids. Tracking and reconstructing eyelids is extremely challenging, as this region exhibits very complex and unique skin deformation where skin is folded under while opening the eye. Furthermore, eyelids are often only partially visible and obstructed due to selfocclusion and eyelashes. Our approach is to combine a geometric deformation model with image data, leveraging multi-view stereo, optical flow, contour tracking and wrinkle detection from local skin appearance. Our deformation model serves as a prior that enables reconstruction of eyelids even under strong self-occlusions caused by rolling and folding skin as the eye opens and closes. The output is a person-specific, time-varying eyelid reconstruction with anatomically plausible deformations. Our high-resolution detailed eyelids couple naturally with current facial performance capture approaches. As a result, our method can largely increase the fidelity of facial capture and the creation of digital doubles.
AU - Bermano, Amit
AU - Beeler, Thabo
AU - Kozlov, Yeara
AU - Bradley, Derek
AU - Bickel, Bernd
AU - Gross, Markus
ID - 1625
IS - 4
TI - Detailed spatio-temporal reconstruction of eyelids
VL - 34
ER -
TY - CONF
AB - This paper introduces "OmniAD," a novel data-driven pipeline to model and acquire the aerodynamics of three-dimensional rigid objects. Traditionally, aerodynamics are examined through elaborate wind tunnel experiments or expensive fluid dynamics computations, and are only measured for a small number of discrete wind directions. OmniAD allows the evaluation of aerodynamic forces, such as drag and lift, for any incoming wind direction using a novel representation based on spherical harmonics. Our datadriven technique acquires the aerodynamic properties of an object simply by capturing its falling motion using a single camera. Once model parameters are estimated, OmniAD enables realistic realtime simulation of rigid bodies, such as the tumbling and gliding of leaves, without simulating the surrounding air. In addition, we propose an intuitive user interface based on OmniAD to interactively design three-dimensional kites that actually fly. Various nontraditional kites were designed to demonstrate the physical validity of our model.
AU - Martin, Tobias
AU - Umetani, Nobuyuki
AU - Bickel, Bernd
ID - 1626
IS - 4
TI - OmniAD: Data-driven omni-directional aerodynamics
VL - 34
ER -
TY - CONF
AB - We present a computational tool for fabrication-oriented design of flexible rod meshes. Given a deformable surface and a set of deformed poses as input, our method automatically computes a printable rod mesh that, once manufactured, closely matches the input poses under the same boundary conditions. The core of our method is formed by an optimization scheme that adjusts the cross-sectional profiles of the rods and their rest centerline in order to best approximate the target deformations. This approach allows us to locally control the bending and stretching resistance of the surface with a single material, yielding high design flexibility and low fabrication cost.
AU - Pérez, Jesús
AU - Thomaszewski, Bernhard
AU - Coros, Stelian
AU - Bickel, Bernd
AU - Canabal, José
AU - Sumner, Robert
AU - Otaduy, Miguel
ID - 1627
IS - 4
TI - Design and fabrication of flexible rod meshes
VL - 34
ER -
TY - CONF
AB - We propose a method for fabricating deformable objects with spatially varying elasticity using 3D printing. Using a single, relatively stiff printer material, our method designs an assembly of smallscale microstructures that have the effect of a softer material at the object scale, with properties depending on the microstructure used in each part of the object. We build on work in the area of metamaterials, using numerical optimization to design tiled microstructures with desired properties, but with the key difference that our method designs families of related structures that can be interpolated to smoothly vary the material properties over a wide range. To create an object with spatially varying elastic properties, we tile the object's interior with microstructures drawn from these families, generating a different microstructure for each cell using an efficient algorithm to select compatible structures for neighboring cells. We show results computed for both 2D and 3D objects, validating several 2D and 3D printed structures using standard material tests as well as demonstrating various example applications.
AU - Schumacher, Christian
AU - Bickel, Bernd
AU - Rys, Jan
AU - Marschner, Steve
AU - Daraio, Chiara
AU - Gross, Markus
ID - 1628
IS - 4
TI - Microstructures to control elasticity in 3D printing
VL - 34
ER -
TY - CONF
AB - We present a method to learn and propagate shape placements in 2D polygonal scenes from a few examples provided by a user. The placement of a shape is modeled as an oriented bounding box. Simple geometric relationships between this bounding box and nearby scene polygons define a feature set for the placement. The feature sets of all example placements are then used to learn a probabilistic model over all possible placements and scenes. With this model, we can generate a new set of placements with similar geometric relationships in any given scene. We introduce extensions that enable propagation and generation of shapes in 3D scenes, as well as the application of a learned modeling session to large scenes without additional user interaction. These concepts allow us to generate complex scenes with thousands of objects with relatively little user interaction.
AU - Guerrero, Paul
AU - Jeschke, Stefan
AU - Wimmer, Michael
AU - Wonka, Peter
ID - 1630
IS - 4
TI - Learning shape placements by example
VL - 34
ER -
TY - CONF
AB - This paper presents a liquid simulation technique that enforces the incompressibility condition using a stream function solve instead of a pressure projection. Previous methods have used stream function techniques for the simulation of detailed single-phase flows, but a formulation for liquid simulation has proved elusive in part due to the free surface boundary conditions. In this paper, we introduce a stream function approach to liquid simulations with novel boundary conditions for free surfaces, solid obstacles, and solid-fluid coupling.
Although our approach increases the dimension of the linear system necessary to enforce incompressibility, it provides interesting and surprising benefits. First, the resulting flow is guaranteed to be divergence-free regardless of the accuracy of the solve. Second, our free-surface boundary conditions guarantee divergence-free motion even in the un-simulated air phase, which enables two-phase flow simulation by only computing a single phase. We implemented this method using a variant of FLIP simulation which only samples particles within a narrow band of the liquid surface, and we illustrate the effectiveness of our method for detailed two-phase flow simulations with complex boundaries, detailed bubble interactions, and two-way solid-fluid coupling.
AU - Ando, Ryoichi
AU - Thuerey, Nils
AU - Wojtan, Christopher J
ID - 1632
IS - 4
TI - A stream function solver for liquid simulations
VL - 34
ER -
TY - CONF
AB - We present a method for simulating brittle fracture under the assumptions of quasi-static linear elastic fracture mechanics (LEFM). Using the boundary element method (BEM) and Lagrangian crack-fronts, we produce highly detailed fracture surfaces. The computational cost of the BEM is alleviated by using a low-resolution mesh and interpolating the resulting stress intensity factors when propagating the high-resolution crack-front.
Our system produces physics-based fracture surfaces with high spatial and temporal resolution, taking spatial variation of material toughness and/or strength into account. It also allows for crack initiation to be handled separately from crack propagation, which is not only more reasonable from a physics perspective, but can also be used to control the simulation.
Separating the resolution of the crack-front from the resolution of the computational mesh increases the efficiency and therefore the amount of visual detail on the resulting fracture surfaces. The BEM also allows us to re-use previously computed blocks of the system matrix.
AU - Hahn, David
AU - Wojtan, Christopher J
ID - 1633
IS - 4
TI - High-resolution brittle fracture simulation with boundary elements
VL - 34
ER -
TY - CONF
AB - Simulating the delightful dynamics of soap films, bubbles, and foams has traditionally required the use of a fully three-dimensional many-phase Navier-Stokes solver, even though their visual appearance is completely dominated by the thin liquid surface. We depart from earlier work on soap bubbles and foams by noting that their dynamics are naturally described by a Lagrangian vortex sheet model in which circulation is the primary variable. This leads us to derive a novel circulation-preserving surface-only discretization of foam dynamics driven by surface tension on a non-manifold triangle mesh. We represent the surface using a mesh-based multimaterial surface tracker which supports complex bubble topology changes, and evolve the surface according to the ambient air flow induced by a scalar circulation field stored on the mesh. Surface tension forces give rise to a simple update rule for circulation, even at non-manifold Plateau borders, based on a discrete measure of signed scalar mean curvature. We further incorporate vertex constraints to enable the interaction of soap films with wires. The result is a method that is at once simple, robust, and efficient, yet able to capture an array of soap films behaviors including foam rearrangement, catenoid collapse, blowing bubbles, and double bubbles being pulled apart.
AU - Da, Fang
AU - Batty, Christopher
AU - Wojtan, Christopher J
AU - Grinspun, Eitan
ID - 1634
IS - 4
TI - Double bubbles sans toil and trouble: discrete circulation-preserving vortex sheets for soap films and foams
VL - 34
ER -
TY - JOUR
AB - We calculate a Ricci curvature lower bound for some classical examples of random walks, namely, a chain on a slice of the n-dimensional discrete cube (the so-called Bernoulli-Laplace model) and the random transposition shuffle of the symmetric group of permutations on n letters.
AU - Erbar, Matthias
AU - Maas, Jan
AU - Tetali, Prasad
ID - 1635
IS - 4
JF - Annales de la faculté des sciences de Toulouse
TI - Discrete Ricci curvature bounds for Bernoulli-Laplace and random transposition models
VL - 24
ER -
TY - CONF
AB - Constraint Satisfaction Problem (CSP) is a fundamental algorithmic problem that appears in many areas of Computer Science. It can be equivalently stated as computing a homomorphism R→ΓΓ between two relational structures, e.g. between two directed graphs. Analyzing its complexity has been a prominent research direction, especially for the fixed template CSPs where the right side ΓΓ is fixed and the left side R is unconstrained.
Far fewer results are known for the hybrid setting that restricts both sides simultaneously. It assumes that R belongs to a certain class of relational structures (called a structural restriction in this paper). We study which structural restrictions are effective, i.e. there exists a fixed template ΓΓ (from a certain class of languages) for which the problem is tractable when R is restricted, and NP-hard otherwise. We provide a characterization for structural restrictions that are closed under inverse homomorphisms. The criterion is based on the chromatic number of a relational structure defined in this paper; it generalizes the standard chromatic number of a graph.
As our main tool, we use the algebraic machinery developed for fixed template CSPs. To apply it to our case, we introduce a new construction called a “lifted language”. We also give a characterization for structural restrictions corresponding to minor-closed families of graphs, extend results to certain Valued CSPs (namely conservative valued languages), and state implications for (valued) CSPs with ordered variables and for the maximum weight independent set problem on some restricted families of graphs.
AU - Kolmogorov, Vladimir
AU - Rolinek, Michal
AU - Takhanov, Rustem
ID - 1636
TI - Effectiveness of structural restrictions for hybrid CSPs
VL - 9472
ER -
TY - CONF
AB - An instance of the Valued Constraint Satisfaction Problem (VCSP) is given by a finite set of variables, a finite domain of labels, and a sum of functions, each function depending on a subset of the variables. Each function can take finite values specifying costs of assignments of labels to its variables or the infinite value, which indicates an infeasible assignment. The goal is to find an assignment of labels to the variables that minimizes the sum. We study, assuming that P ≠ NP, how the complexity of this very general problem depends on the set of functions allowed in the instances, the so-called constraint language. The case when all allowed functions take values in {0, ∞} corresponds to ordinary CSPs, where one deals only with the feasibility issue and there is no optimization. This case is the subject of the Algebraic CSP Dichotomy Conjecture predicting for which constraint languages CSPs are tractable (i.e. solvable in polynomial time) and for which NP-hard. The case when all allowed functions take only finite values corresponds to finite-valued CSP, where the feasibility aspect is trivial and one deals only with the optimization issue. The complexity of finite-valued CSPs was fully classified by Thapper and Zivny. An algebraic necessary condition for tractability of a general-valued CSP with a fixed constraint language was recently given by Kozik and Ochremiak. As our main result, we prove that if a constraint language satisfies this algebraic necessary condition, and the feasibility CSP (i.e. the problem of deciding whether a given instance has a feasible solution) corresponding to the VCSP with this language is tractable, then the VCSP is tractable. The algorithm is a simple combination of the assumed algorithm for the feasibility CSP and the standard LP relaxation. As a corollary, we obtain that a dichotomy for ordinary CSPs would imply a dichotomy for general-valued CSPs.
AU - Kolmogorov, Vladimir
AU - Krokhin, Andrei
AU - Rolinek, Michal
ID - 1637
TI - The complexity of general-valued CSPs
ER -