TY - JOUR
AB - Avian forelimb digit homology remains one of the standard themes in comparative biology and EvoDevo research. In order to resolve the apparent contradictions between embryological and paleontological evidence a variety of hypotheses have been presented in recent years. The proposals range from excluding birds from the dinosaur clade, to assignments of homology by different criteria, or even assuming a hexadactyl tetrapod limb ground state. At present two approaches prevail: the frame shift hypothesis and the pyramid reduction hypothesis. While the former postulates a homeotic shift of digit identities, the latter argues for a gradual bilateral reduction of phalanges and digits. Here we present a new model that integrates elements from both hypotheses with the existing experimental and fossil evidence. We start from the main feature common to both earlier concepts, the initiating ontogenetic event: reduction and loss of the anterior-most digit. It is proposed that a concerted mechanism of molecular regulation and developmental mechanics is capable of shifting the boundaries of hoxD expression in embryonic forelimb buds as well as changing the digit phenotypes. Based on a distinction between positional (topological) and compositional (phenotypic) homology criteria, we argue that the identity of the avian digits is II, III, IV, despite a partially altered phenotype. Finally, we introduce an alternative digit reduction scheme that reconciles the current fossil evidence with the presented molecular-morphogenetic model. Our approach identifies specific experiments that allow to test whether gene expression can be shifted and digit phenotypes can be altered by induced digit loss or digit gain.
AU - Capek, Daniel
AU - Metscher, Brian
AU - Müller, Gerd
ID - 2248
IS - 1
JF - Journal of Experimental Zoology Part B: Molecular and Developmental Evolution
SN - 15525007
TI - Thumbs down: A molecular-morphogenetic approach to avian digit homology
VL - 322
ER -
TY - JOUR
AB - The unfolded protein response (UPR) is a signaling network triggered by overload of protein-folding demand in the endoplasmic reticulum (ER), a condition termed ER stress. The UPR is critical for growth and development; nonetheless, connections between the UPR and other cellular regulatory processes remain largely unknown. Here, we identify a link between the UPR and the phytohormone auxin, a master regulator of plant physiology. We show that ER stress triggers down-regulation of auxin receptors and transporters in Arabidopsis thaliana. We also demonstrate that an Arabidopsis mutant of a conserved ER stress sensor IRE1 exhibits defects in the auxin response and levels. These data not only support that the plant IRE1 is required for auxin homeostasis, they also reveal a species-specific feature of IRE1 in multicellular eukaryotes. Furthermore, by establishing that UPR activation is reduced in mutants of ER-localized auxin transporters, including PIN5, we define a long-neglected biological significance of ER-based auxin regulation. We further examine the functional relationship of IRE1 and PIN5 by showing that an ire1 pin5 triple mutant enhances defects of UPR activation and auxin homeostasis in ire1 or pin5. Our results imply that the plant UPR has evolved a hormone-dependent strategy for coordinating ER function with physiological processes.
AU - Chen, Yani
AU - Aung, Kyaw
AU - Rolčík, Jakub
AU - Walicki, Kathryn
AU - Friml, Jirí
AU - Brandizzí, Federica
ID - 2249
IS - 1
JF - Plant Journal
SN - 09607412
TI - Inter-regulation of the unfolded protein response and auxin signaling
VL - 77
ER -
TY - JOUR
AB - The genome sequences of new viruses often contain many "orphan" or "taxon-specific" proteins apparently lacking homologs. However, because viral proteins evolve very fast, commonly used sequence similarity detection methods such as BLAST may overlook homologs. We analyzed a data set of proteins from RNA viruses characterized as "genus specific" by BLAST. More powerful methods developed recently, such as HHblits or HHpred (available through web-based, user-friendly interfaces), could detect distant homologs of a quarter of these proteins, suggesting that these methods should be used to annotate viral genomes. In-depth manual analyses of a subset of the remaining sequences, guided by contextual information such as taxonomy, gene order, or domain cooccurrence, identified distant homologs of another third. Thus, a combination of powerful automated methods and manual analyses can uncover distant homologs of many proteins thought to be orphans. We expect these methodological results to be also applicable to cellular organisms, since they generally evolve much more slowly than RNA viruses. As an application, we reanalyzed the genome of a bee pathogen, Chronic bee paralysis virus (CBPV). We could identify homologs of most of its proteins thought to be orphans; in each case, identifying homologs provided functional clues. We discovered that CBPV encodes a domain homologous to the Alphavirus methyltransferase-guanylyltransferase; a putative membrane protein, SP24, with homologs in unrelated insect viruses and insect-transmitted plant viruses having different morphologies (cileviruses, higreviruses, blunerviruses, negeviruses); and a putative virion glycoprotein, ORF2, also found in negeviruses. SP24 and ORF2 are probably major structural components of the virionsd.
AU - Kuchibhatla, Durga
AU - Sherman, Westley
AU - Chung, Betty
AU - Cook, Shelley
AU - Schneider, Georg
AU - Eisenhaber, Birgit
AU - Karlin, David
ID - 2250
IS - 1
JF - Journal of Virology
SN - 0022538X
TI - Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently "orphan" viral proteins
VL - 88
ER -
TY - JOUR
AB - Sharp wave/ripple (SWR, 150–250 Hz) hippocampal events have long been postulated to be involved in memory consolidation. However, more recent work has investigated SWRs that occur during active waking behaviour: findings that suggest that SWRs may also play a role in cell assembly strengthening or spatial working memory. Do such theories of SWR function apply to animal learning? This review discusses how general theories linking SWRs to memory-related function may explain circuit mechanisms related to rodent spatial learning and to the associated stabilization of new cognitive maps.
AU - Csicsvari, Jozsef L
AU - Dupret, David
ID - 2251
IS - 1635
JF - Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences
SN - 09628436
TI - Sharp wave/ripple network oscillations and learning-associated hippocampal maps
VL - 369
ER -
TY - JOUR
AB - The pattern of inheritance and mechanism of sex determination can have important evolutionary consequences. We studied probabilistic sex determination in the ciliate Tetrahymena thermophila, which was previously shown to cause evolution of skewed sex ratios. We find that the genetic background alters the sex determination patterns of mat alleles in heterozygotes and that allelic interaction can differentially influence the expression probability of the 7 sexes. We quantify the dominance relationships between several mat alleles and find that A-type alleles, which specify sex I, are indeed recessive to B-type alleles, which are unable to specify that sex. Our results provide additional support for the presence of modifier loci and raise implications for the dynamics of sex ratios in populations of T. thermophila.
AU - Phadke, Sujal
AU - Paixao, Tiago
AU - Pham, Tuan
AU - Pham, Stephanie
AU - Zufall, Rebecca
ID - 2252
IS - 1
JF - Journal of Heredity
SN - 00221503
TI - Genetic background alters dominance relationships between mat alleles in the ciliate Tetrahymena Thermophila
VL - 105
ER -
TY - JOUR
AB - Plant growth is achieved predominantly by cellular elongation, which is thought to be controlled on several levels by apoplastic auxin. Auxin export into the apoplast is achieved by plasma membrane efflux catalysts of the PIN-FORMED (PIN) and ATP-binding cassette protein subfamily B/phosphor- glycoprotein (ABCB/PGP) classes; the latter were shown to depend on interaction with the FKBP42, TWISTED DWARF1 (TWD1). Here by using a transgenic approach in combination with phenotypical, biochemical and cell biological analyses we demonstrate the importance of a putative C-terminal in-plane membrane anchor of TWD1 in the regulation of ABCB-mediated auxin transport. In contrast with dwarfed twd1 loss-of-function alleles, TWD1 gain-of-function lines that lack a putative in-plane membrane anchor (HA-TWD1-Ct) show hypermorphic plant architecture, characterized by enhanced stem length and leaf surface but reduced shoot branching. Greater hypocotyl length is the result of enhanced cell elongation that correlates with reduced polar auxin transport capacity for HA-TWD1-Ct. As a consequence, HA-TWD1-Ct displays higher hypocotyl auxin accumulation, which is shown to result in elevated auxin-induced cell elongation rates. Our data highlight the importance of C-terminal membrane anchoring for TWD1 action, which is required for specific regulation of ABCB-mediated auxin transport. These data support a model in which TWD1 controls lateral ABCB1-mediated export into the apoplast, which is required for auxin-mediated cell elongation.
AU - Bailly, Aurélien
AU - Wang, Bangjun
AU - Zwiewka, Marta
AU - Pollmann, Stephan
AU - Schenck, Daniel
AU - Lüthen, Hartwig
AU - Schulz, Alexander
AU - Friml, Jirí
AU - Geisler, Markus
ID - 2253
IS - 1
JF - Plant Journal
SN - 09607412
TI - Expression of TWISTED DWARF1 lacking its in-plane membrane anchor leads to increased cell elongation and hypermorphic growth
VL - 77
ER -
TY - JOUR
AB - Theta-gamma network oscillations are thought to represent key reference signals for information processing in neuronal ensembles, but the underlying synaptic mechanisms remain unclear. To address this question, we performed whole-cell (WC) patch-clamp recordings from mature hippocampal granule cells (GCs) in vivo in the dentate gyrus of anesthetized and awake rats. GCs in vivo fired action potentials at low frequency, consistent with sparse coding in the dentate gyrus. GCs were exposed to barrages of fast AMPAR-mediated excitatory postsynaptic currents (EPSCs), primarily relayed from the entorhinal cortex, and inhibitory postsynaptic currents (IPSCs), presumably generated by local interneurons. EPSCs exhibited coherence with the field potential predominantly in the theta frequency band, whereas IPSCs showed coherence primarily in the gamma range. Action potentials in GCs were phase locked to network oscillations. Thus, theta-gamma-modulated synaptic currents may provide a framework for sparse temporal coding of information in the dentate gyrus.
AU - Pernia-Andrade, Alejandro
AU - Jonas, Peter M
ID - 2254
IS - 1
JF - Neuron
SN - 08966273
TI - Theta-gamma-modulated synaptic currents in hippocampal granule cells in vivo define a mechanism for network oscillations
VL - 81
ER -
TY - JOUR
AB - Motivated by applications in biology, we present an algorithm for estimating the length of tube-like shapes in 3-dimensional Euclidean space. In a first step, we combine the tube formula of Weyl with integral geometric methods to obtain an integral representation of the length, which we approximate using a variant of the Koksma-Hlawka Theorem. In a second step, we use tools from computational topology to decrease the dependence on small perturbations of the shape. We present computational experiments that shed light on the stability and the convergence rate of our algorithm.
AU - Edelsbrunner, Herbert
AU - Pausinger, Florian
ID - 2255
IS - 1
JF - Journal of Mathematical Imaging and Vision
SN - 09249907
TI - Stable length estimates of tube-like shapes
VL - 50
ER -
TY - JOUR
AB - Maximum entropy models are the least structured probability distributions that exactly reproduce a chosen set of statistics measured in an interacting network. Here we use this principle to construct probabilistic models which describe the correlated spiking activity of populations of up to 120 neurons in the salamander retina as it responds to natural movies. Already in groups as small as 10 neurons, interactions between spikes can no longer be regarded as small perturbations in an otherwise independent system; for 40 or more neurons pairwise interactions need to be supplemented by a global interaction that controls the distribution of synchrony in the population. Here we show that such “K-pairwise” models—being systematic extensions of the previously used pairwise Ising models—provide an excellent account of the data. We explore the properties of the neural vocabulary by: 1) estimating its entropy, which constrains the population's capacity to represent visual information; 2) classifying activity patterns into a small set of metastable collective modes; 3) showing that the neural codeword ensembles are extremely inhomogenous; 4) demonstrating that the state of individual neurons is highly predictable from the rest of the population, allowing the capacity for error correction.
AU - Tkacik, Gasper
AU - Marre, Olivier
AU - Amodei, Dario
AU - Schneidman, Elad
AU - Bialek, William
AU - Berry, Michael
ID - 2257
IS - 1
JF - PLoS Computational Biology
SN - 1553734X
TI - Searching for collective behavior in a large network of sensory neurons
VL - 10
ER -
TY - JOUR
AB - To reveal the full potential of human pluripotent stem cells, new methods for rapid, site-specific genomic engineering are needed. Here, we describe a system for precise genetic modification of human embryonic stem cells (ESCs) and induced pluripotent stem cells (iPSCs). We identified a novel human locus, H11, located in a safe, intergenic, transcriptionally active region of chromosome 22, as the recipient site, to provide robust, ubiquitous expression of inserted genes. Recipient cell lines were established by site-specific placement of a ‘landing pad’ cassette carrying attP sites for phiC31 and Bxb1 integrases at the H11 locus by spontaneous or TALEN-assisted homologous recombination. Dual integrase cassette exchange (DICE) mediated by phiC31 and Bxb1 integrases was used to insert genes of interest flanked by phiC31 and Bxb1 attB sites at the H11 locus, replacing the landing pad. This system provided complete control over content, direction and copy number of inserted genes, with a specificity of 100%. A series of genes, including mCherry and various combinations of the neural transcription factors LMX1a, FOXA2 and OTX2, were inserted in recipient cell lines derived from H9 ESC, as well as iPSC lines derived from a Parkinson’s disease patient and a normal sibling control. The DICE system offers rapid, efficient and precise gene insertion in ESC and iPSC and is particularly well suited for repeated modifications of the same locus.
AU - Zhu, Fangfang
AU - Gamboa, Matthew
AU - Farruggio, Alfonso
AU - Hippenmeyer, Simon
AU - Tasic, Bosiljka
AU - Schüle, Birgitt
AU - Chen Tsai, Yanru
AU - Calos, Michele
ID - 2261
IS - 5
JF - Nucleic Acids Research
TI - DICE, an efficient system for iterative genomic editing in human pluripotent stem cells
VL - 42
ER -
TY - CHAP
AB - Coordinated migration of newly-born neurons to their target territories is essential for correct neuronal circuit assembly in the developing brain. Although a cohort of signaling pathways has been implicated in the regulation of cortical projection neuron migration, the precise molecular mechanisms and how a balanced interplay of cell-autonomous and non-autonomous functions of candidate signaling molecules controls the discrete steps in the migration process, are just being revealed. In this chapter, I will focally review recent advances that improved our understanding of the cell-autonomous and possible cell-nonautonomous functions of the evolutionarily conserved LIS1/NDEL1-complex in regulating the sequential steps of cortical projection neuron migration. I will then elaborate on the emerging concept that the Reelin signaling pathway, acts exactly at precise stages in the course of cortical projection neuron migration. Lastly, I will discuss how finely tuned transcriptional programs and downstream effectors govern particular aspects in driving radial migration at discrete stages and how they regulate the precise positioning of cortical projection neurons in the developing cerebral cortex.
AU - Hippenmeyer, Simon
ED - Nguyen, Laurent
ID - 2265
T2 - Cellular and Molecular Control of Neuronal Migration
TI - Molecular pathways controlling the sequential steps of cortical projection neuron migration
VL - 800
ER -
TY - CONF
AB - Energies with high-order non-submodular interactions have been shown to be very useful in vision due to their high modeling power. Optimization of such energies, however, is generally NP-hard. A naive approach that works for small problem instances is exhaustive search, that is, enumeration of all possible labelings of the underlying graph. We propose a general minimization approach for large graphs based on enumeration of labelings of certain small patches.
This partial enumeration technique reduces complex high-order energy formulations to pairwise Constraint Satisfaction Problems with unary costs (uCSP), which can be efficiently solved using standard methods like TRW-S. Our approach outperforms a number of existing state-of-the-art algorithms on well known difficult problems (e.g. curvature regularization, stereo, deconvolution); it gives near global minimum and better speed.
Our main application of interest is curvature regularization. In the context of segmentation, our partial enumeration technique allows to evaluate curvature directly on small patches using a novel integral geometry approach.
AU - Olsson, Carl
AU - Ulen, Johannes
AU - Boykov, Yuri
AU - Kolmogorov, Vladimir
ID - 2275
TI - Partial enumeration and curvature regularization
ER -
TY - JOUR
AB - GABAergic inhibitory interneurons control fundamental aspects of neuronal network function. Their functional roles are assumed to be defined by the identity of their input synapses, the architecture of their dendritic tree, the passive and active membrane properties and finally the nature of their postsynaptic targets. Indeed, interneurons display a high degree of morphological and physiological heterogeneity. However, whether their morphological and physiological characteristics are correlated and whether interneuron diversity can be described by a continuum of GABAergic cell types or by distinct classes has remained unclear. Here we perform a detailed morphological and physiological characterization of GABAergic cells in the dentate gyrus, the input region of the hippocampus. To achieve an unbiased and efficient sampling and classification we used knock-in mice expressing the enhanced green fluorescent protein (eGFP) in glutamate decarboxylase 67 (GAD67)-positive neurons and performed cluster analysis. We identified five interneuron classes, each of them characterized by a distinct set of anatomical and physiological parameters. Cross-correlation analysis further revealed a direct relation between morphological and physiological properties indicating that dentate gyrus interneurons fall into functionally distinct classes which may differentially control neuronal network activity.
AU - Hosp, Jonas
AU - Strüber, Michael
AU - Yanagawa, Yuchio
AU - Obata, Kunihiko
AU - Vida, Imre
AU - Jonas, Peter M
AU - Bartos, Marlene
ID - 2285
IS - 2
JF - Hippocampus
TI - Morpho-physiological criteria divide dentate gyrus interneurons into classes
VL - 23
ER -
TY - JOUR
AB - Invasive alien parasites and pathogens are a growing threat to biodiversity worldwide, which can contribute to the extinction of endemic species. On the Galápagos Islands, the invasive parasitic fly Philornis downsi poses a major threat to the endemic avifauna. Here, we investigated the influence of this parasite on the breeding success of two Darwin's finch species, the warbler finch (Certhidea olivacea) and the sympatric small tree finch (Camarhynchus parvulus), on Santa Cruz Island in 2010 and 2012. While the population of the small tree finch appeared to be stable, the warbler finch has experienced a dramatic decline in population size on Santa Cruz Island since 1997. We aimed to identify whether warbler finches are particularly vulnerable during different stages of the breeding cycle. Contrary to our prediction, breeding success was lower in the small tree finch than in the warbler finch. In both species P. downsi had a strong negative impact on breeding success and our data suggest that heavy rain events also lowered the fledging success. On the one hand parents might be less efficient in compensating their chicks' energy loss due to parasitism as they might be less efficient in foraging on days of heavy rain. On the other hand, intense rainfalls might lead to increased humidity and more rapid cooling of the nests. In the case of the warbler finch we found that the control of invasive plant species with herbicides had a significant additive negative impact on the breeding success. It is very likely that the availability of insects (i.e. food abundance) is lower in such controlled areas, as herbicide usage led to the removal of the entire understory. Predation seems to be a minor factor in brood loss.
AU - Cimadom, Arno
AU - Ulloa, Angel
AU - Meidl, Patrick
AU - Zöttl, Markus
AU - Zöttl, Elisabet
AU - Fessl, Birgit
AU - Nemeth, Erwin
AU - Dvorak, Michael
AU - Cunninghame, Francesca
AU - Tebbich, Sabine
ID - 468
IS - 9
JF - PLoS One
TI - Invasive parasites habitat change and heavy rainfall reduce breeding success in Darwin's finches
VL - 9
ER -
TY - CONF
AB - First cycle games (FCG) are played on a finite graph by two players who push a token along the edges until a vertex is repeated, and a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of labels of the edges (or nodes) forming this cycle. These games are traditionally of interest because of their connection with infinite-duration games such as parity and mean-payoff games. We study the memory requirements for winning strategies of FCGs and certain associated infinite duration games. We exhibit a simple FCG that is not memoryless determined (this corrects a mistake in Memoryless determinacy of parity and mean payoff games: a simple proof by Bj⋯orklund, Sandberg, Vorobyov (2004) that claims that FCGs for which Y is closed under cyclic permutations are memoryless determined). We show that θ (n)! memory (where n is the number of nodes in the graph), which is always sufficient, may be necessary to win some FCGs. On the other hand, we identify easy to check conditions on Y (i.e., Y is closed under cyclic permutations, and both Y and its complement are closed under concatenation) that are sufficient to ensure that the corresponding FCGs and their associated infinite duration games are memoryless determined. We demonstrate that many games considered in the literature, such as mean-payoff, parity, energy, etc., satisfy these conditions. On the complexity side, we show (for efficiently computable Y) that while solving FCGs is in PSPACE, solving some families of FCGs is PSPACE-hard.
AU - Aminof, Benjamin
AU - Rubin, Sasha
ID - 475
T2 - Electronic Proceedings in Theoretical Computer Science, EPTCS
TI - First cycle games
VL - 146
ER -
TY - JOUR
AB - Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help.
AU - Chatterjee, Krishnendu
AU - Henzinger, Monika
AU - Krinninger, Sebastian
AU - Nanongkai, Danupon
ID - 535
IS - 3
JF - Algorithmica
TI - Polynomial time algorithms for energy games with special weight structures
VL - 70
ER -
TY - JOUR
AB - Transgenerational effects are broader than only parental relationships. Despite mounting evidence that multigenerational effects alter phenotypic and life-history traits, our understanding of how they combine to determine fitness is not well developed because of the added complexity necessary to study them. Here, we derive a quantitative genetic model of adaptation to an extraordinary new environment by an additive genetic component, phenotypic plasticity, maternal and grandmaternal effects. We show how, at equilibrium, negative maternal and negative grandmaternal effects maximize expected population mean fitness. We define negative transgenerational effects as those that have a negative effect on trait expression in the subsequent generation, that is, they slow, or potentially reverse, the expected evolutionary dynamic. When maternal effects are positive, negative grandmaternal effects are preferred. As expected under Mendelian inheritance, the grandmaternal effects have a lower impact on fitness than the maternal effects, but this dual inheritance model predicts a more complex relationship between maternal and grandmaternal effects to constrain phenotypic variance and so maximize expected population mean fitness in the offspring.
AU - Prizak, Roshan
AU - Ezard, Thomas
AU - Hoyle, Rebecca
ID - 537
IS - 15
JF - Ecology and Evolution
TI - Fitness consequences of maternal and grandmaternal effects
VL - 4
ER -
TY - GEN
AB - Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing.
In this paper, we study compositional properties of the IOCO-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the IOCO conformance relation, the resulting methodology can be applied to a broader class of systems.
AU - Daca, Przemyslaw
AU - Henzinger, Thomas A
AU - Krenn, Willibald
AU - Nickovic, Dejan
ID - 5411
SN - 2664-1690
TI - Compositional specifications for IOCO testing
ER -
TY - GEN
AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability.
We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.
We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.
AU - Chatterjee, Krishnendu
AU - Daca, Przemyslaw
AU - Chmelik, Martin
ID - 5412
SN - 2664-1690
TI - CEGAR for qualitative analysis of probabilistic systems
ER -
TY - GEN
AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability.
We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.
We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.
AU - Chatterjee, Krishnendu
AU - Daca, Przemyslaw
AU - Chmelik, Martin
ID - 5413
SN - 2664-1690
TI - CEGAR for qualitative analysis of probabilistic systems
ER -
TY - GEN
AB - We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability.
We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.
We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis leads to significant improvements.
AU - Chatterjee, Krishnendu
AU - Daca, Przemyslaw
AU - Chmelik, Martin
ID - 5414
SN - 2664-1690
TI - CEGAR for qualitative analysis of probabilistic systems
ER -
TY - GEN
AB - Recently there has been a significant effort to add quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Otop, Jan
ID - 5415
SN - 2664-1690
TI - Nested weighted automata
ER -
TY - GEN
AB - As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.The contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem.
AU - Henzinger, Thomas A
AU - Otop, Jan
ID - 5416
SN - 2664-1690
TI - Model measuring for hybrid systems
ER -
TY - GEN
AB - We define the model-measuring problem: given a model M and specification φ, what is the maximal distance ρ such that all models M'within distance ρ from M satisfy (or violate)φ. The model measuring problem presupposes a distance function on models. We concentrate on automatic distance functions, which are defined by weighted automata.
The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification, and robustness problems that measure how much a model can be perturbed without violating the specification.
We show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved.
We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for standard word and tree automata by the optimal-weight question for the weighted versions of these automata. We consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging.
We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications.
AU - Henzinger, Thomas A
AU - Otop, Jan
ID - 5417
SN - 2664-1690
TI - From model checking to model measuring
ER -
TY - GEN
AB - We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. Our results have tight connections with partial-observation stochastic games for which we derive new complexity results.
AU - Chatterjee, Krishnendu
AU - Doyen, Laurent
ID - 5418
SN - 2664-1690
TI - Games with a weak adversary
ER -
TY - GEN
AB - We consider the reachability and shortest path problems on low tree-width graphs, with n nodes, m edges, and tree-width t, on a standard RAM with wordsize W. We use O to hide polynomial factors of the inverse of the Ackermann function. Our main contributions are three fold:
1. For reachability, we present an algorithm that requires O(n·t2·log(n/t)) preprocessing time, O(n·(t·log(n/t))/W) space, and O(t/W) time for pair queries and O((n·t)/W) time for single-source queries. Note that for constant t our algorithm uses O(n·logn) time for preprocessing; and O(n/W) time for single-source queries, which is faster than depth first search/breath first search (after the preprocessing).
2. We present an algorithm for shortest path that requires O(n·t2) preprocessing time, O(n·t) space, and O(t2) time for pair queries and O(n·t) time single-source queries.
3. We give a space versus query time trade-off algorithm for shortest path that, given any constant >0, requires O(n·t2) preprocessing time, O(n·t2) space, and O(n1−·t2) time for pair queries.
Our algorithms improve all existing results, and use very simple data structures.
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
AU - Pavlogiannis, Andreas
ID - 5419
SN - 2664-1690
TI - Improved algorithms for reachability and shortest path on low tree-width graphs
ER -
TY - GEN
AB - We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy).
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
ID - 5420
SN - 2664-1690
TI - The value 1 problem for concurrent mean-payoff games
ER -
TY - GEN
AB - Evolution occurs in populations of reproducing individuals. The structure of the population affects the outcome of the evolutionary process. Evolutionary graph theory is a powerful approach to study this phenomenon. There are two graphs. The interaction graph specifies who interacts with whom in the context of evolution. The replacement graph specifies who competes with whom for reproduction. The vertices of the two graphs are the same, and each vertex corresponds to an individual. A key quantity is the fixation probability of a new mutant. It is defined as the probability that a newly introduced mutant (on a single vertex) generates a lineage of offspring which eventually takes over the entire population of resident individuals. The basic computational questions are as follows: (i) the qualitative question asks whether the fixation probability is positive; and (ii) the quantitative approximation question asks for an approximation of the fixation probability. Our main results are: (1) We show that the qualitative question is NP-complete and the quantitative approximation question is #P-hard in the special case when the interaction and the replacement graphs coincide and even with the restriction that the resident individuals do not reproduce (which corresponds to an invading population taking over an empty structure). (2) We show that in general the qualitative question is PSPACE-complete and the quantitative approximation question is PSPACE-hard and can be solved in exponential time.
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
AU - Nowak, Martin
ID - 5421
SN - 2664-1690
TI - The complexity of evolution on graphs
ER -
TY - GEN
AB - Notes from the Third Plenary for the Research Data Alliance in Dublin, Ireland on March 26 to 28, 2014 with focus on starting an institutional research data repository.
AU - Porsche, Jana
ID - 5422
TI - Notes from Research Data Alliance Plenary Meeting in Dublin, Ireland
ER -
TY - GEN
AB - We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm- deadline real-time tasks based on multi-objective graphs: Given a taskset and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. a clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including D(over), that have been proposed in the past, for various tasksets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are tasksets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.
AU - Chatterjee, Krishnendu
AU - Kössler, Alexander
AU - Pavlogiannis, Andreas
AU - Schmid, Ulrich
ID - 5423
SN - 2664-1690
TI - A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks
ER -
TY - GEN
AB - We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty.
AU - Chatterjee, Krishnendu
AU - Chmelik, Martin
AU - Gupta, Raghav
AU - Kanodia, Ayush
ID - 5424
SN - 2664-1690
TI - Qualitative analysis of POMDPs with temporal logic specifications for robotics applications
ER -
TY - GEN
AB - We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objective we study asks to minimize the expected total cost till the target set is reached, while ensuring that the target set is reached almost-surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost and the bound is double exponential; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst-case running time of our algorithm is double exponential, we also present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples of interest.
AU - Anonymous, 1
AU - Anonymous, 2
AU - Anonymous, 3
AU - Anonymous, 4
ID - 5425
SN - 2664-1690
TI - Optimal cost almost-sure reachability in POMDPs
ER -
TY - GEN
AB - We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty.
AU - Chatterjee, Krishnendu
AU - Chmelik, Martin
AU - Gupta, Raghav
AU - Kanodia, Ayush
ID - 5426
SN - 2664-1690
TI - Qualitative analysis of POMDPs with temporal logic specifications for robotics applications
ER -
TY - GEN
AB - We consider graphs with n nodes together with their tree-decomposition that has b = O ( n ) bags and width t , on the standard RAM computational model with wordsize W = Θ (log n ) . Our contributions are two-fold: Our first contribution is an algorithm that given a graph and its tree-decomposition as input, computes a binary and balanced tree-decomposition of width at most 4 · t + 3 of the graph in O ( b ) time and space, improving a long-standing (from 1992) bound of O ( n · log n ) time for constant treewidth graphs. Our second contribution is on reachability queries for low treewidth graphs. We build on our tree-balancing algorithm and present a data-structure for graph reachability that requires O ( n · t 2 ) preprocessing time, O ( n · t ) space, and O ( d t/ log n e ) time for pair queries, and O ( n · t · log t/ log n ) time for single-source queries. For constant t our data-structure uses O ( n ) time for preprocessing, O (1) time for pair queries, and O ( n/ log n ) time for single-source queries. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries.
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
AU - Pavlogiannis, Andreas
ID - 5427
SN - 2664-1690
TI - Optimal tree-decomposition balancing and reachability on low treewidth graphs
ER -
TY - GEN
AB - Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms.
In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Otop, Jan
AU - Velner, Yaron
ID - 5428
SN - 2664-1690
TI - Quantitative fair simulation games
ER -
TY - CHAP
AB - Mechanically coupled cells can generate forces driving cell and tissue morphogenesis during development. Visualization and measuring of these forces is of major importance to better understand the complexity of the biomechanic processes that shape cells and tissues. Here, we describe how UV laser ablation can be utilized to quantitatively assess mechanical tension in different tissues of the developing zebrafish and in cultures of primary germ layer progenitor cells ex vivo.
AU - Smutny, Michael
AU - Behrndt, Martin
AU - Campinho, Pedro
AU - Ruprecht, Verena
AU - Heisenberg, Carl-Philipp J
ED - Nelson, Celeste
ID - 6178
SN - 1064-3745
T2 - Tissue Morphogenesis
TI - UV laser ablation to measure cell and tissue-generated forces in the zebrafish embryo in vivo and ex vivo
VL - 1189
ER -
TY - JOUR
AB - We prove the universality of the β-ensembles with convex analytic potentials and for any β >
0, i.e. we show that the spacing distributions of log-gases at any inverse temperature β coincide with those of the Gaussian β-ensembles.
AU - Erdös, László
AU - Bourgade, Paul
AU - Yau, Horng
ID - 2699
IS - 6
JF - Duke Mathematical Journal
TI - Universality of general β-ensembles
VL - 163
ER -
TY - JOUR
AB - Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω ω -regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on vector addition systems with states. Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.
AU - Chatterjee, Krishnendu
AU - Randour, Mickael
AU - Raskin, Jean
ID - 2716
IS - 3-4
JF - Acta Informatica
TI - Strategy synthesis for multi-dimensional quantitative objectives
VL - 51
ER -
TY - JOUR
AB - A robust combiner for hash functions takes two candidate implementations and constructs a hash function which is secure as long as at least one of the candidates is secure. So far, hash function combiners only aim at preserving a single property such as collision-resistance or pseudorandomness. However, when hash functions are used in protocols like TLS they are often required to provide several properties simultaneously. We therefore put forward the notion of robust multi-property combiners and elaborate on different definitions for such combiners. We then propose a combiner that provably preserves (target) collision-resistance, pseudorandomness, and being a secure message authentication code. This combiner satisfies the strongest notion we propose, which requires that the combined function satisfies every security property which is satisfied by at least one of the underlying hash function. If the underlying hash functions have output length n, the combiner has output length 2 n. This basically matches a known lower bound for black-box combiners for collision-resistance only, thus the other properties can be achieved without penalizing the length of the hash values. We then propose a combiner which also preserves the property of being indifferentiable from a random oracle, slightly increasing the output length to 2 n+ω(log n). Moreover, we show how to augment our constructions in order to make them also robust for the one-wayness property, but in this case require an a priory upper bound on the input length.
AU - Fischlin, Marc
AU - Lehmann, Anja
AU - Pietrzak, Krzysztof Z
ID - 2852
IS - 3
JF - Journal of Cryptology
TI - Robust multi-property combiners for hash functions
VL - 27
ER -
TY - CONF
AB - Persistent homology is a recent grandchild of homology that has found use in
science and engineering as well as in mathematics. This paper surveys the method as well
as the applications, neglecting completeness in favor of highlighting ideas and directions.
AU - Edelsbrunner, Herbert
AU - Morozovy, Dmitriy
ID - 2905
TI - Persistent homology: Theory and practice
ER -
TY - BOOK
AB - This monograph presents a short course in computational geometry and topology. In the first part the book covers Voronoi diagrams and Delaunay triangulations, then it presents the theory of alpha complexes which play a crucial role in biology. The central part of the book is the homology theory and their computation, including the theory of persistence which is indispensable for applications, e.g. shape reconstruction. The target audience comprises researchers and practitioners in mathematics, biology, neuroscience and computer science, but the book may also be beneficial to graduate students of these fields.
AU - Edelsbrunner, Herbert
ID - 6853
SN - 2191-530X
TI - A Short Course in Computational Geometry and Topology
ER -
TY - GEN
AU - Huszár, Kristóf
AU - Rolinek, Michal
ID - 7038
TI - Playful Math - An introduction to mathematical games
ER -
TY - JOUR
AB - We propose a method for propagating edit operations in 2D vector graphics, based on geometric relationship functions. These functions quantify the geometric relationship of a point to a polygon, such as the distance to the boundary or the direction to the closest corner vertex. The level sets of the relationship functions describe points with the same relationship to a polygon. For a given query point, we first determine a set of relationships to local features, construct all level sets for these relationships, and accumulate them. The maxima of the resulting distribution are points with similar geometric relationships. We show extensions to handle mirror symmetries, and discuss the use of relationship functions as local coordinate systems. Our method can be applied, for example, to interactive floorplan editing, and it is especially useful for large layouts, where individual edits would be cumbersome. We demonstrate populating 2D layouts with tens to hundreds of objects by propagating relatively few edit operations.
AU - Guerrero, Paul
AU - Jeschke, Stefan
AU - Wimmer, Michael
AU - Wonka, Peter
ID - 1629
IS - 2
JF - ACM Transactions on Graphics
TI - Edit propagation using geometric relationship functions
VL - 33
ER -
TY - CONF
AB - We extend the notion of verifiable random functions (VRF) to constrained VRFs, which generalize the concept of constrained pseudorandom functions, put forward by Boneh and Waters (Asiacrypt’13), and independently by Kiayias et al. (CCS’13) and Boyle et al. (PKC’14), who call them delegatable PRFs and functional PRFs, respectively. In a standard VRF the secret key sk allows one to evaluate a pseudorandom function at any point of its domain; in addition, it enables computation of a non-interactive proof that the function value was computed correctly. In a constrained VRF from the key sk one can derive constrained keys skS for subsets S of the domain, which allow computation of function values and proofs only at points in S. After formally defining constrained VRFs, we derive instantiations from the multilinear-maps-based constrained PRFs by Boneh and Waters, yielding a VRF with constrained keys for any set that can be decided by a polynomial-size circuit. Our VRFs have the same function values as the Boneh-Waters PRFs and are proved secure under the same hardness assumption, showing that verifiability comes at no cost. Constrained (functional) VRFs were stated as an open problem by Boyle et al.
AU - Fuchsbauer, Georg
ED - Abdalla, Michel
ED - De Prisco, Roberto
ID - 1643
T2 - SCN 2014
TI - Constrained Verifiable Random Functions
VL - 8642
ER -
TY - CONF
AB - In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.
AU - Gupta, Ashutosh
AU - Popeea, Corneliu
AU - Rybalchenko, Andrey
ID - 1702
T2 - Electronic Proceedings in Theoretical Computer Science, EPTCS
TI - Generalised interpolation by solving recursion free-horn clauses
VL - 169
ER -
TY - CONF
AB - It has been long argued that, because of inherent ambiguity and noise, the brain needs to represent uncertainty in the form of probability distributions. The neural encoding of such distributions remains however highly controversial. Here we present a novel circuit model for representing multidimensional real-valued distributions using a spike based spatio-temporal code. Our model combines the computational advantages of the currently competing models for probabilistic codes and exhibits realistic neural responses along a variety of classic measures. Furthermore, the model highlights the challenges associated with interpreting neural activity in relation to behavioral uncertainty and points to alternative population-level approaches for the experimental validation of distributed representations.
AU - Savin, Cristina
AU - Denève, Sophie
ID - 1708
IS - January
TI - Spatio-temporal representations of uncertainty in spiking neural networks
VL - 3
ER -
TY - JOUR
AB - The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.
AU - Cerny, Pavol
AU - Chmelik, Martin
AU - Henzinger, Thomas A
AU - Radhakrishna, Arjun
ID - 1733
IS - 3
JF - Theoretical Computer Science
TI - Interface simulation distances
VL - 560
ER -
TY - CHAP
AB - The generation of asymmetry, at both cellular and tissue level, is one of the most essential capabilities of all eukaryotic organisms. It mediates basically all multicellular development ranging from embryogenesis and de novo organ formation till responses to various environmental stimuli. In plants, the awe-inspiring number of such processes is regulated by phytohormone auxin and its directional, cell-to-cell transport. The mediators of this transport, PIN auxin transporters, are asymmetrically localized at the plasma membrane, and this polar localization determines the directionality of intercellular auxin flow. Thus, auxin transport contributes crucially to the generation of local auxin gradients or maxima, which instruct given cell to change its developmental program. Here, we introduce and discuss the molecular components and cellular mechanisms regulating the generation and maintenance of cellular PIN polarity, as the general hallmarks of cell polarity in plants.
AU - Baster, Pawel
AU - Friml, Jiří
ED - Zažímalová, Eva
ED - Petrášek, Jan
ED - Benková, Eva
ID - 1806
T2 - Auxin and Its Role in Plant Development
TI - Auxin on the road navigated by cellular PIN polarity
ER -
TY - JOUR
AB - Watermarking techniques for vector graphics dislocate vertices in order to embed imperceptible, yet detectable, statistical features into the input data. The embedding process may result in a change of the topology of the input data, e.g., by introducing self-intersections, which is undesirable or even disastrous for many applications. In this paper we present a watermarking framework for two-dimensional vector graphics that employs conventional watermarking techniques but still provides the guarantee that the topology of the input data is preserved. The geometric part of this framework computes so-called maximum perturbation regions (MPR) of vertices. We propose two efficient algorithms to compute MPRs based on Voronoi diagrams and constrained triangulations. Furthermore, we present two algorithms to conditionally correct the watermarked data in order to increase the watermark embedding capacity and still guarantee topological correctness. While we focus on the watermarking of input formed by straight-line segments, one of our approaches can also be extended to circular arcs. We conclude the paper by demonstrating and analyzing the applicability of our framework in conjunction with two well-known watermarking techniques.
AU - Huber, Stefan
AU - Held, Martin
AU - Meerwald, Peter
AU - Kwitt, Roland
ID - 1816
IS - 1
JF - International Journal of Computational Geometry and Applications
TI - Topology-preserving watermarking of vector graphics
VL - 24
ER -
TY - JOUR
AB - We review recent progress towards a rigorous understanding of the Bogoliubov approximation for bosonic quantum many-body systems. We focus, in particular, on the excitation spectrum of a Bose gas in the mean-field (Hartree) limit. A list of open problems will be discussed at the end.
AU - Seiringer, Robert
ID - 1821
IS - 7
JF - Journal of Mathematical Physics
TI - Bose gases, Bose-Einstein condensation, and the Bogoliubov approximation
VL - 55
ER -