TY - JOUR AB - Guided cell movement is essential for development and integrity of animals and crucially involved in cellular immune responses. Leukocytes are professional migratory cells that can navigate through most types of tissues and sense a wide range of directional cues. The responses of these cells to attractants have been mainly explored in tissue culture settings. How leukocytes make directional decisions in situ, within the challenging environment of a tissue maze, is less understood. Here we review recent advances in how leukocytes sense chemical cues in complex tissue settings and make links with paradigms of directed migration in development and Dictyostelium discoideum amoebae. AU - Sarris, Milka AU - Sixt, Michael K ID - 1687 IS - 10 JF - Current Opinion in Cell Biology TI - Navigating in tissue mazes: Chemoattractant interpretation in complex environments VL - 36 ER - TY - CONF AB - Given a graph G cellularly embedded on a surface Σ of genus g, a cut graph is a subgraph of G such that cutting Σ along G yields a topological disk. We provide a fixed parameter tractable approximation scheme for the problem of computing the shortest cut graph, that is, for any ε > 0, we show how to compute a (1 + ε) approximation of the shortest cut graph in time f(ε, g)n3. Our techniques first rely on the computation of a spanner for the problem using the technique of brick decompositions, to reduce the problem to the case of bounded tree-width. Then, to solve the bounded tree-width case, we introduce a variant of the surface-cut decomposition of Rué, Sau and Thilikos, which may be of independent interest. AU - Cohen Addad, Vincent AU - De Mesmay, Arnaud N ID - 1685 TI - A fixed parameter tractable approximation scheme for the optimal cut graph of a surface VL - 9294 ER - TY - JOUR AB - We estimate the selection constant in the following geometric selection theorem by Pach: For every positive integer d, there is a constant (Formula presented.) such that whenever (Formula presented.) are n-element subsets of (Formula presented.), we can find a point (Formula presented.) and subsets (Formula presented.) for every i∈[d+1], each of size at least cdn, such that p belongs to all rainbowd-simplices determined by (Formula presented.) simplices with one vertex in each Yi. We show a super-exponentially decreasing upper bound (Formula presented.). The ideas used in the proof of the upper bound also help us to prove Pach’s theorem with (Formula presented.), which is a lower bound doubly exponentially decreasing in d (up to some polynomial in the exponent). For comparison, Pach’s original approach yields a triply exponentially decreasing lower bound. On the other hand, Fox, Pach, and Suk recently obtained a hypergraph density result implying a proof of Pach’s theorem with (Formula presented.). In our construction for the upper bound, we use the fact that the minimum solid angle of every d-simplex is super-exponentially small. This fact was previously unknown and might be of independent interest. For the lower bound, we improve the ‘separation’ part of the argument by showing that in one of the key steps only d+1 separations are necessary, compared to 2d separations in the original proof. We also provide a measure version of Pach’s theorem. AU - Karasev, Roman AU - Kynčl, Jan AU - Paták, Pavel AU - Patakova, Zuzana AU - Tancer, Martin ID - 1688 IS - 3 JF - Discrete & Computational Geometry TI - Bounds for Pach's selection theorem and for the minimum solid angle in a simplex VL - 54 ER - TY - JOUR AB - We consider the satisfiability problem for modal logic over first-order definable classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We provide a full classification of Horn formulae with respect to the complexity of the corresponding satisfiability problem. It turns out, that except for the trivial case of inconsistent formulae, local satisfiability is eitherNP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or ExpTime-complete. We also show that the finite satisfiability problem for modal logic over Horn definable classes of frames is decidable. On the negative side, we show undecidability of two related problems. First, we exhibit a simple universal three-variable formula defining the class of frames over which modal logic is undecidable. Second, we consider the satisfiability problem of bimodal logic over Horn definable classes of frames, and also present a formula leading to undecidability. AU - Michaliszyn, Jakub AU - Otop, Jan AU - Kieroňski, Emanuel ID - 1680 IS - 1 JF - ACM Transactions on Computational Logic TI - On the decidability of elementary modal logics VL - 17 ER - TY - JOUR AB - We study the problem of robust satisfiability of systems of nonlinear equations, namely, whether for a given continuous function f:K→ ℝn on a finite simplicial complex K and α > 0, it holds that each function g: K → ℝn such that ||g - f || ∞ < α, has a root in K. Via a reduction to the extension problem of maps into a sphere, we particularly show that this problem is decidable in polynomial time for every fixed n, assuming dimK ≤ 2n - 3. This is a substantial extension of previous computational applications of topological degree and related concepts in numerical and interval analysis. Via a reverse reduction, we prove that the problem is undecidable when dim K > 2n - 2, where the threshold comes from the stable range in homotopy theory. For the lucidity of our exposition, we focus on the setting when f is simplexwise linear. Such functions can approximate general continuous functions, and thus we get approximation schemes and undecidability of the robust satisfiability in other possible settings. AU - Franek, Peter AU - Krcál, Marek ID - 1682 IS - 4 JF - Journal of the ACM TI - Robust satisfiability of systems of equations VL - 62 ER - TY - JOUR AB - The 1 MDa, 45-subunit proton-pumping NADH-ubiquinone oxidoreductase (complex I) is the largest complex of the mitochondrial electron transport chain. The molecular mechanism of complex I is central to the metabolism of cells, but has yet to be fully characterized. The last two years have seen steady progress towards this goal with the first atomic-resolution structure of the entire bacterial complex I, a 5 Å cryo-electron microscopy map of bovine mitochondrial complex I and a ∼3.8 Å resolution X-ray crystallographic study of mitochondrial complex I from yeast Yarrowia lipotytica. In this review we will discuss what we have learned from these studies and what remains to be elucidated. AU - Letts, Jame A AU - Sazanov, Leonid A ID - 1683 IS - 8 JF - Current Opinion in Structural Biology TI - Gaining mass: The structure of respiratory complex I-from bacterial towards mitochondrial versions VL - 33 ER - TY - JOUR AU - Kiermaier, Eva AU - Sixt, Michael K ID - 1686 IS - 6252 JF - Science TI - Fragmented communication between immune cells: Neutrophils blaze a trail with migratory cues for T cells to follow to sites of infection VL - 349 ER - TY - CONF AB - Computing an approximation of the reachable states of a hybrid system is a challenge, mainly because overapproximating the solutions of ODEs with a finite number of sets does not scale well. Using template polyhedra can greatly reduce the computational complexity, since it replaces complex operations on sets with a small number of optimization problems. However, the use of templates may make the over-approximation too conservative. Spurious transitions, which are falsely considered reachable, are particularly detrimental to performance and accuracy, and may exacerbate the state explosion problem. In this paper, we examine how spurious transitions can be avoided with minimal computational effort. To this end, detecting spurious transitions is reduced to the well-known problem of showing that two convex sets are disjoint by finding a hyperplane that separates them. We generalize this to owpipes by considering hyperplanes that evolve with time in correspondence to the dynamics of the system. The approach is implemented in the model checker SpaceEx and demonstrated on examples. AU - Frehse, Goran AU - Bogomolov, Sergiy AU - Greitschus, Marius AU - Strump, Thomas AU - Podelski, Andreas ID - 1692 SN - 978-1-4503-3433-4 T2 - Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control TI - Eliminating spurious transitions in reachability with support functions ER - TY - JOUR AB - Quantum interference between energetically close states is theoretically investigated, with the state structure being observed via laser spectroscopy. In this work, we focus on hyperfine states of selected hydrogenic muonic isotopes, and on how quantum interference affects the measured Lamb shift. The process of photon excitation and subsequent photon decay is implemented within the framework of nonrelativistic second-order perturbation theory. Due to its experimental interest, calculations are performed for muonic hydrogen, deuterium, and helium-3. We restrict our analysis to the case of photon scattering by incident linear polarized photons and the polarization of the scattered photons not being observed. We conclude that while quantum interference effects can be safely neglected in muonic hydrogen and helium-3, in the case of muonic deuterium there are resonances with close proximity, where quantum interference effects can induce shifts up to a few percent of the linewidth, assuming a pointlike detector. However, by taking into account the geometry of the setup used by the CREMA collaboration, this effect is reduced to less than 0.2% of the linewidth in all possible cases, which makes it irrelevant at the present level of accuracy. © 2015 American Physical Society. AU - Amaro, Pedro AU - Franke, Beatrice AU - Krauth, Julian AU - Diepold, Marc AU - Fratini, Filippo AU - Safari, Laleh AU - Machado, Jorge AU - Antognini, Aldo AU - Kottmann, Franz AU - Indelicato, Paul AU - Pohl, Randolf AU - Santos, José ID - 1693 IS - 2 JF - Physical Review A TI - Quantum interference effects in laser spectroscopy of muonic hydrogen, deuterium, and helium-3 VL - 92 ER - TY - CONF AB - A number of powerful and scalable hybrid systems model checkers have recently emerged. Although all of them honor roughly the same hybrid systems semantics, they have drastically different model description languages. This situation (a) makes it difficult to quickly evaluate a specific hybrid automaton model using the different tools, (b) obstructs comparisons of reachability approaches, and (c) impedes the widespread application of research results that perform model modification and could benefit many of the tools. In this paper, we present Hyst, a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation passes that serve to both ease the translation and potentially improve reachability results for the supported tools. Although these model transformation passes could be implemented within each tool, the Hyst approach provides a single place for model modification, generating modified input sources for the unmodified target tools. Our evaluation demonstrates Hyst is capable of automatically translating benchmarks in several classes (including affine and nonlinear hybrid automata) to the input formats of several tools. Additionally, we illustrate a general model transformation pass based on pseudo-invariants implemented in Hyst that illustrates the reachability improvement. AU - Bak, Stanley AU - Bogomolov, Sergiy AU - Johnson, Taylor ID - 1690 TI - HYST: A source transformation and translation tool for hybrid automaton models ER -