TY - JOUR
AB - We consider two systems (α1, …, αm) and (β1, …,βn) of simple curves drawn on a compact two-dimensional surface M with boundary. Each αi and each βj is either an arc meeting the boundary of M at its two endpoints, or a closed curve. The αi are pairwise disjoint except for possibly sharing endpoints, and similarly for the βj. We want to “untangle” the βj from the ai by a self-homeomorphism of M; more precisely, we seek a homeomorphism φ:M→M fixing the boundary of M pointwise such that the total number of crossings of the ai with the φ(βj) is as small as possible. This problem is motivated by an application in the algorithmic theory of embeddings and 3-manifolds. We prove that if M is planar, i.e., a sphere with h ≥ 0 boundary components (“holes”), then O(mn) crossings can be achieved (independently of h), which is asymptotically tight, as an easy lower bound shows. In general, for an arbitrary (orientable or nonorientable) surface M with h holes and of (orientable or nonorientable) genus g ≥ 0, we obtain an O((m + n)4) upper bound, again independent of h and g. The proofs rely, among other things, on a result concerning simultaneous planar drawings of graphs by Erten and Kobourov.
AU - Matoušek, Jiří
AU - Sedgwick, Eric
AU - Tancer, Martin
AU - Wagner, Uli
ID - 1411
IS - 1
JF - Israel Journal of Mathematics
TI - Untangling two systems of noncrossing curves
VL - 212
ER -
TY - JOUR
AB - We consider Conditional random fields (CRFs) with pattern-based potentials defined on a chain. In this model the energy of a string (labeling) (Formula presented.) is the sum of terms over intervals [i, j] where each term is non-zero only if the substring (Formula presented.) equals a prespecified pattern w. Such CRFs can be naturally applied to many sequence tagging problems. We present efficient algorithms for the three standard inference tasks in a CRF, namely computing (i) the partition function, (ii) marginals, and (iii) computing the MAP. Their complexities are respectively (Formula presented.), (Formula presented.) and (Formula presented.) where L is the combined length of input patterns, (Formula presented.) is the maximum length of a pattern, and D is the input alphabet. This improves on the previous algorithms of Ye et al. (NIPS, 2009) whose complexities are respectively (Formula presented.), (Formula presented.) and (Formula presented.), where (Formula presented.) is the number of input patterns. In addition, we give an efficient algorithm for sampling, and revisit the case of MAP with non-positive weights.
AU - Kolmogorov, Vladimir
AU - Takhanov, Rustem
ID - 1794
IS - 1
JF - Algorithmica
TI - Inference algorithms for pattern-based CRFs on sequence data
VL - 76
ER -
TY - JOUR
AB - Most entropy notions H(.) like Shannon or min-entropy satisfy a chain rule stating that for random variables X,Z, and A we have H(X|Z,A)≥H(X|Z)−|A|. That is, by conditioning on A the entropy of X can decrease by at most the bitlength |A| of A. Such chain rules are known to hold for some computational entropy notions like Yao’s and unpredictability-entropy. For HILL entropy, the computational analogue of min-entropy, the chain rule is of special interest and has found many applications, including leakage-resilient cryptography, deterministic encryption, and memory delegation. These applications rely on restricted special cases of the chain rule. Whether the chain rule for conditional HILL entropy holds in general was an open problem for which we give a strong negative answer: we construct joint distributions (X,Z,A), where A is a distribution over a single bit, such that the HILL entropy H HILL (X|Z) is large but H HILL (X|Z,A) is basically zero.
Our counterexample just makes the minimal assumption that NP⊈P/poly. Under the stronger assumption that injective one-way function exist, we can make all the distributions efficiently samplable.
Finally, we show that some more sophisticated cryptographic objects like lossy functions can be used to sample a distribution constituting a counterexample to the chain rule making only a single invocation to the underlying object.
AU - Krenn, Stephan
AU - Pietrzak, Krzysztof Z
AU - Wadia, Akshay
AU - Wichs, Daniel
ID - 1479
IS - 3
JF - Computational Complexity
TI - A counterexample to the chain rule for conditional HILL entropy
VL - 25
ER -
TY - JOUR
AB - Most migrating cells extrude their front by the force of actin polymerization. Polymerization requires an initial nucleation step, which is mediated by factors establishing either parallel filaments in the case of filopodia or branched filaments that form the branched lamellipodial network. Branches are considered essential for regular cell motility and are initiated by the Arp2/3 complex, which in turn is activated by nucleation-promoting factors of the WASP and WAVE families. Here we employed rapid amoeboid crawling leukocytes and found that deletion of the WAVE complex eliminated actin branching and thus lamellipodia formation. The cells were left with parallel filaments at the leading edge, which translated, depending on the differentiation status of the cell, into a unipolar pointed cell shape or cells with multiple filopodia. Remarkably, unipolar cells migrated with increased speed and enormous directional persistence, while they were unable to turn towards chemotactic gradients. Cells with multiple filopodia retained chemotactic activity but their migration was progressively impaired with increasing geometrical complexity of the extracellular environment. These findings establish that diversified leading edge protrusions serve as explorative structures while they slow down actual locomotion.
AU - Leithner, Alexander F
AU - Eichner, Alexander
AU - Müller, Jan
AU - Reversat, Anne
AU - Brown, Markus
AU - Schwarz, Jan
AU - Merrin, Jack
AU - De Gorter, David
AU - Schur, Florian
AU - Bayerl, Jonathan
AU - De Vries, Ingrid
AU - Wieser, Stefan
AU - Hauschild, Robert
AU - Lai, Frank
AU - Moser, Markus
AU - Kerjaschki, Dontscho
AU - Rottner, Klemens
AU - Small, Victor
AU - Stradal, Theresia
AU - Sixt, Michael K
ID - 1321
JF - Nature Cell Biology
TI - Diversified actin protrusions promote environmental exploration but are dispensable for locomotion of leukocytes
VL - 18
ER -
TY - JOUR
AB - Autism spectrum disorders (ASD) are a group of genetic disorders often overlapping with other neurological conditions. We previously described abnormalities in the branched-chain amino acid (BCAA) catabolic pathway as a cause of ASD. Here, we show that the solute carrier transporter 7a5 (SLC7A5), a large neutral amino acid transporter localized at the blood brain barrier (BBB), has an essential role in maintaining normal levels of brain BCAAs. In mice, deletion of Slc7a5 from the endothelial cells of the BBB leads to atypical brain amino acid profile, abnormal mRNA translation, and severe neurological abnormalities. Furthermore, we identified several patients with autistic traits and motor delay carrying deleterious homozygous mutations in the SLC7A5 gene. Finally, we demonstrate that BCAA intracerebroventricular administration ameliorates abnormal behaviors in adult mutant mice. Our data elucidate a neurological syndrome defined by SLC7A5 mutations and support an essential role for the BCAA in human brain function.
AU - Tarlungeanu, Dora-Clara
AU - Deliu, Elena
AU - Dotter, Christoph
AU - Kara, Majdi
AU - Janiesch, Philipp
AU - Scalise, Mariafrancesca
AU - Galluccio, Michele
AU - Tesulov, Mateja
AU - Morelli, Emanuela
AU - Sönmez, Fatma
AU - Bilgüvar, Kaya
AU - Ohgaki, Ryuichi
AU - Kanai, Yoshikatsu
AU - Johansen, Anide
AU - Esharif, Seham
AU - Ben Omran, Tawfeg
AU - Topcu, Meral
AU - Schlessinger, Avner
AU - Indiveri, Cesare
AU - Duncan, Kent
AU - Caglayan, Ahmet
AU - Günel, Murat
AU - Gleeson, Joseph
AU - Novarino, Gaia
ID - 1183
IS - 6
JF - Cell
TI - Impaired amino acid transport at the blood brain barrier is a cause of autism spectrum disorder
VL - 167
ER -
TY - JOUR
AB - Optogenetics and photopharmacology enable the spatio-temporal control of cell and animal behavior by light. Although red light offers deep-tissue penetration and minimal phototoxicity, very few red-light-sensitive optogenetic methods are currently available. We have now developed a red-light-induced homodimerization domain. We first showed that an optimized sensory domain of the cyanobacterial phytochrome 1 can be expressed robustly and without cytotoxicity in human cells. We then applied this domain to induce the dimerization of two receptor tyrosine kinases—the fibroblast growth factor receptor 1 and the neurotrophin receptor trkB. This new optogenetic method was then used to activate the MAPK/ERK pathway non-invasively in mammalian tissue and in multicolor cell-signaling experiments. The light-controlled dimerizer and red-light-activated receptor tyrosine kinases will prove useful to regulate a variety of cellular processes with light. Go deep with red: The sensory domain (S) of the cyanobacterial phytochrome 1 (CPH1) was repurposed to induce the homodimerization of proteins in living cells by red light. By using this domain, light-activated protein kinases were engineered that can be activated orthogonally from many fluorescent proteins and through mammalian tissue. Pr/Pfr=red-/far-red-absorbing state of CPH1.
AU - Gschaider-Reichhart, Eva
AU - Inglés Prieto, Álvaro
AU - Tichy, Alexandra-Madelaine
AU - Mckenzie, Catherine
AU - Janovjak, Harald L
ID - 1441
IS - 21
JF - Angewandte Chemie - International Edition
TI - A phytochrome sensory domain permits receptor activation by red light
VL - 55
ER -
TY - CONF
AB - In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.
AU - Jiang, Yu
AU - Liu, Han
AU - Song, Houbing
AU - Kong, Hui
AU - Gu, Ming
AU - Sun, Jiaguang
AU - Sha, Lui
ID - 1205
TI - Safety assured formal model driven design of the multifunction vehicle bus controller
VL - 9995
ER -
TY - CONF
AB - Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic.
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
ID - 478
TI - The complexity of deciding legality of a single step of magic: The gathering
VL - 285
ER -
TY - CONF
AB - Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for -approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements.
AU - Chatterjee, Krishnendu
AU - Doyen, Laurent
ID - 480
TI - Perfect-information stochastic games with generalized mean-payoff objectives
VL - 05-08-July-2016
ER -
TY - CONF
AB - We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.
AU - Daca, Przemyslaw
AU - Henzinger, Thomas A
AU - Kretinsky, Jan
AU - Petrov, Tatjana
ID - 1234
TI - Faster statistical model checking for unbounded temporal properties
VL - 9636
ER -