TY - JOUR
AB - Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators ⋄ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path.
We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics.
AU - de Alfaro, Luca
AU - Faella, Marco
AU - Thomas Henzinger
AU - Majumdar, Ritankar S
AU - Stoelinga, Mariëlle
ID - 4625
IS - 1
JF - Theoretical Computer Science
TI - Model checking discounted temporal properties
VL - 345
ER -
TY - CONF
AB - We present the first demonstration of Jozsa's "counterfactual computation", using an optical Grover's search algorithm. We put the algorithm in a superposition of 'running' and 'not-running', obtaining information even though the algorithm does not run.
AU - Onur Hosten
AU - Rakher, Matthew T
AU - Barreiro, Julio T
AU - Peters, Nicholas A
AU - Kwiat, Paul G
ID - 575
TI - Counterfactual quantum computation
VL - 1
ER -
TY - JOUR
AB - A current challenge in neuroscience is to bridge the gaps between genes, proteins, neurons, neural circuits, and behavior in a single animal model. The nematode Caenorhabditis elegans has unique features that facilitate this synthesis. Its nervous system includes exactly 302 neurons, and their pattern of synaptic connectivity is known. With only five olfactory neurons, C. elegans can dynamically respond to dozens of attractive and repellant odors. Thermosensory neurons enable the nematode to remember its cultivation temperature and to track narrow isotherms. Polymodal sensory neurons detect a wide range of nociceptive cues and signal robust escape responses. Pairing of sensory stimuli leads to long-lived changes in behavior consistent with associative learning. Worms exhibit social behaviors and complex ultradian rhythms driven by Ca2+ oscillators with clock-like properties. Genetic analysis has identified gene products required for nervous system function and elucidated the molecular and neural bases of behaviors.
AU - de Bono, Mario
AU - Villu Maricq, Andres
ID - 6153
JF - Annual Review of Neuroscience
SN - 0147-006X
TI - Neuronal substrates of complex behaviors in C. elegans
VL - 28
ER -
TY - JOUR
AU - Cheung, Benny H.H.
AU - Cohen, Merav
AU - Rogers, Candida
AU - Albayram, Onder
AU - de Bono, Mario
ID - 6154
IS - 10
JF - Current Biology
SN - 0960-9822
TI - Experience-dependent modulation of C. elegans behavior by ambient oxygen
VL - 15
ER -
TY - JOUR
AB - Genetically encoded fluorescent probes of neural activity represent new promising tools for systems neuroscience. Here, we present a comparative in vivo analysis of 10 different genetically encoded calcium indicators, as well as the pH-sensitive synapto-pHluorin. We analyzed their fluorescence changes in presynaptic boutons of the Drosophila larval neuromuscular junction. Robust neural activity did not result in any or noteworthy fluorescence changes when Flash-Pericam, Camgaroo-1, and Camgaroo-2 were expressed. However, calculated on the raw data, fractional fluorescence changes up to 18% were reported by synapto-pHluorin, Yellow Cameleon 2.0, 2.3, and 3.3, Inverse-Pericam, GCaMP1.3, GCaMP1.6, and the troponin C-based calcium sensor TN-L15. The response characteristics of all of these indicators differed considerably from each other, with GCaMP1.6 reporting high rates of neural activity with the largest and fastest fluorescence changes. However, GCaMP1.6 suffered from photobleaching, whereas the fluorescence signals of the double-chromophore indicators were in general smaller but more photostable and reproducible, with TN-L15 showing the fastest rise of the signals at lower activity rates. We show for GCaMP1.3 and YC3.3 that an expanded range of neural activity evoked fairly linear fluorescence changes and a corresponding linear increase in the signal-to-noise ratio (SNR). The expression level of the indicator biased the signal kinetics and SNR, whereas the signal amplitude was independent. The presented data will be useful for in vivo experiments with respect to the selection of an appropriate indicator, as well as for the correct interpretation of the optical signals.
AU - Reiff, Dierk F
AU - Ihring, Alexandra
AU - Guerrero, Giovanna
AU - Isacoff, Ehud Y
AU - Maximilian Jösch
AU - Nakai, Junichi
AU - Borst, Alexander
ID - 1298
IS - 19
JF - Journal of Neuroscience
TI - In vivo performance of genetically encoded indicators of neural activity in flies
VL - 25
ER -
TY - CHAP
AB - The paper surveys the mirror symmetry conjectures of Hausel-Thaddeus and Hausel-Rodriguez-Villegas concerning the equality of certain Hodge numbers of SL(n, ℂ) vs. PGL(n, ℂ) flat connections and character varieties for curves, respectively. Several new results and conjectures and their relations to works of Hitchin, Gothen, Garsia-Haiman and Earl-Kirwan are explained. These use the representation theory of finite groups of Lie-type via the arithmetic of character varieties and lead to an unexpected conjecture for a Hard Lefschetz theorem for their cohomology.
AU - Tamas Hausel
ID - 1444
T2 - Geometric Methods in Algebra and Number Theory
TI - Mirror symmetry and Langlands duality in the non-Abelian Hodge theory of a curve
VL - 235
ER -
TY - JOUR
AB - Building on a recent paper [8], here we argue that the combinatorics of matroids are intimately related to the geometry and topology of toric hyperkähler varieties. We show that just like toric varieties occupy a central role in Stanley’s proof for the necessity of McMullen’s conjecture (or g-inequalities) about the classification of face vectors of simplicial polytopes, the topology of toric hyperkähler varieties leads to new restrictions on face vectors of matroid complexes. Namely in this paper we will give two proofs that the injectivity part of the Hard Lefschetz theorem survives for toric hyperkähler varieties. We explain how this implies the g-inequalities for rationally representable matroids. We show how the geometrical intuition in the first proof, coupled with results of Chari [3], leads to a proof of the g-inequalities for general matroid complexes, which is a recent result of Swartz [20]. The geometrical idea in the second proof will show that a pure O-sequence should satisfy the g-inequalities, thus showing that our result is in fact a consequence of a long-standing conjecture of Stanley.
AU - Tamas Hausel
ID - 1447
IS - 1
JF - Open Mathematics
TI - Quaternionic geometry of matroids
VL - 3
ER -
TY - JOUR
AB - We study an integration theory in circle equivariant cohomology in order to prove a theorem relating the cohomology ring of a hyperkähler quotient to the cohomology ring of the quotient by a maximal abelian subgroup, analogous to a theorem of Martin for symplectic quotients. We discuss applications of this theorem to quiver varieties, and compute as an example the ordinary and equivariant cohomology rings of a hyperpolygon space.
AU - Tamas Hausel
AU - Proudfoot, Nicholas J
ID - 1463
IS - 1
JF - Topology
TI - Abelianization for hyperkähler quotients
VL - 44
ER -
TY - JOUR
AB - Amino acid composition of proteins varies substantially between taxa and, thus, can evolve. For example, proteins from organisms with (G+C)-rich (or (A+T)-rich) genomes contain more (or fewer) amino acids encoded by (G+C)-rich codons. However, no universal trends in ongoing changes of amino acid frequencies have been reported. We compared sets of orthologous proteins encoded by triplets of closely related genomes from 15 taxa representing all three domains of life (Bacteria, Archaea and Eukaryota), and used phylogenies to polarize amino acid substitutions. Cys, Met, His, Ser and Phe accrue in at least 14 taxa, whereas Pro, Ala, Glu and Gly are consistently lost. The same nine amino acids are currently accrued or lost in human proteins, as shown by analysis of non-synonymous single-nucleotide polymorphisms. All amino acids with declining frequencies are thought to be among the first incorporated into the genetic code; conversely, all amino acids with increasing frequencies, except Ser, were probably recruited late. Thus, expansion of initially under-represented amino acids, which began over 3,400 million years ago, apparently continues to this day.
AU - Jordan, Ingo K
AU - Fyodor Kondrashov
AU - Adzhubeǐ, Ivan A
AU - Wolf, Yuri I
AU - Koonin, Eugene V
AU - Kondrashov, Alexey S
AU - Sunyaev, Shamil R
ID - 893
IS - 7026
JF - Nature
TI - A universal trend of amino acid gain and loss in protein evolution
VL - 433
ER -
TY - JOUR
AU - Guzmán, José
AU - Gerevich, Zoltan
AU - Hengstler, Jan
AU - Illes, Peter
AU - Kleemann, Werner
ID - 3720
IS - 4
JF - Synapse
TI - P2Y1 receptors inhibit both strength and plasticity of glutamatergic synaptic neurotransmission in the rat prefrontal cortex.
VL - 57
ER -
TY - JOUR
AB - Recent advances in atomic force microscopy allowed globular and membrane proteins to be mechanically unfolded on a single-molecule level. Presented is an extension to the existing force spectroscopy experiments. While unfolding single bacteriorhodopsins from native purple membranes, small oscillation amplitudes (6–9nm) were supplied to the vertical displacement of the cantilever at a frequency of 3kHz. The phase and amplitude response of the cantilever-protein system was converted to reveal the elastic (conservative) and viscous (dissipative) contributions to the unfolding process. The elastic response (stiffness) of the extended parts of the protein were in the range of a few tens pN/nm and could be well described by the derivative of the wormlike chain model. Discrete events in the viscous response coincided with the unfolding of single secondary structure elements and were in the range of 1μNs/m. In addition, these force modulation spectroscopy experiments revealed novel mechanical unfolding intermediates of bacteriorhodopsin. We found that kinks result in a loss of unfolding cooperativity in transmembrane helices. Reconstructing force-distance spectra by the integration of amplitude-distance spectra verified their position, offering a novel approach to detect intermediates during the forced unfolding of single proteins.
AU - Harald Janovjak
AU - Mueller, Daniel J
AU - Humphris, Andrew D
ID - 3721
IS - 2
JF - Biophysical Journal
TI - Molecular force modulation spectroscopy revealing the dynamic response of single bacteriorhodopsins
VL - 88
ER -
TY - JOUR
AB - In an age of increasingly large data sets, investigators in many different disciplines have turned to clustering as a tool for data analysis and exploration. Existing clustering methods, however, typically depend on several nontrivial assumptions about the structure of data. Here, we reformulate the clustering problem from an information theoretic perspective that avoids many of these assumptions. In particular, our formulation obviates the need for defining a cluster "prototype," does not require an a priori similarity metric, is invariant to changes in the representation of the data, and naturally captures nonlinear relations. We apply this approach to different domains and find that it consistently produces clusters that are more coherent than those extracted by existing algorithms. Finally, our approach provides a way of clustering based on collective notions of similarity rather than the traditional pairwise measures.
AU - Slonim,N.
AU - Atwal,G.
AU - Gasper Tkacik
AU - Bialek, William S
ID - 3741
IS - 51
JF - PNAS
TI - Information-based clustering
VL - 102
ER -
TY - GEN
AB - We address the practical problems of estimating the information relations that characterize large networks. Building on methods developed for analysis of the neural code, we show that reliable estimates of mutual information can be obtained with manageable computational effort. The same methods allow estimation of higher order, multi-information terms. These ideas are illustrated by analyses of gene expression, financial markets, and consumer preferences. In each case, information theoretic measures correlate with independent, intuitive measures of the underlying structures in the system.
AU - Slonim,Noam
AU - Atwal,Gurinder S
AU - Gasper Tkacik
AU - Bialek, William S
ID - 3746
T2 - ArXiv
TI - Estimating mutual information and multi-information in large networks
ER -
TY - JOUR
AB - Characterizing the dynamics of specific RNA levels requires real-time RNA profiling in a single cell. We show that the combination of a synthetic modular genetic system with fluorescence correlation spectroscopy allows us to directly measure in real time the activity of any specific promoter in prokaryotes. Using a simple inducible gene expression system, we found that induced RNA levels within a single bacterium of Escherichia coli exhibited a pulsating profile in response to a steady input of inducer. The genetic deletion of an efflux pump system, a key determinant of antibiotic resistance, altered the pulsating transcriptional dynamics and caused overexpression of induced RNA. In contrast with population measurements, real-time RNA profiling permits identifying relationships between genotypes and transcriptional dynamics that are accessible only at the level of the single cell.
AU - Le,Thuc T.
AU - Harlepp, Sébastien
AU - Calin Guet
AU - Dittmar,Kimberly
AU - Emonet,Thierry
AU - Pan,Tao
AU - Cluzel,Philippe
ID - 3753
IS - 26
JF - PNAS
TI - Real-time RNA profiling within a single bacterium
VL - 102
ER -
TY - JOUR
AB - The generation of realistic motion satisfying user-defined requirements is one of the most important goals of computer animation. Our aim in this paper is the synthesis of realistic, controllable motion for lightweight natural objects in a gaseous medium. We formulate this problem as a large-scale spacetime optimization with user controls and fluid motion equations as constraints. We have devised novel and effective methods to make this large optimization tractable. Initial trajectories are generated with data-driven synthesis based on stylistic motion planning. Smoothed particle hydrodynamics (SPH) is used during optimization to produce fluid simulations at a reasonable computational cost, while interesting vortex-based fluid motion is generated by recording the presence of vortices in the initial trajectories and maintaining them through optimization. Object rotations are refined as a postprocess to enhance the visual quality of the results. We demonstrate our techniques on a number of animations involving single or multiple objects.
AU - Shi, Lin
AU - Yu, Yizhou
AU - Wojtan, Christopher J
AU - Chenney, Stephen
ID - 3763
IS - 7
JF - The Visual Computer
TI - Controllable motion synthesis in a gaseous medium
VL - 21
ER -
TY - JOUR
AB - Action potentials in central neurons are initiated near the axon initial segment, propagate into the axon, and finally invade the presynaptic terminals, where they trigger transmitter release. Voltage-gated Na(+) channels are key determinants of excitability, but Na(+) channel density and properties in axons and presynaptic terminals of cortical neurons have not been examined yet. In hippocampal mossy fiber boutons, which emerge from parent axons en passant, Na(+) channels are very abundant, with an estimated number of approximately 2000 channels per bouton. Presynaptic Na(+) channels show faster inactivation kinetics than somatic channels, suggesting differences between subcellular compartments of the same cell. Computational analysis of action potential propagation in axon-multibouton structures reveals that Na(+) channels in boutons preferentially amplify the presynaptic action potential and enhance Ca(2+) inflow, whereas Na(+) channels in axons control the reliability and speed of propagation. Thus, presynaptic and axonal Na(+) channels contribute differentially to mossy fiber synaptic transmission.
AU - Engel, Dominique
AU - Peter Jonas
ID - 3808
IS - 3
JF - Neuron
TI - Presynaptic action potential amplification by voltage-gated Na+ channels in hippocampal mossy fiber boutons
VL - 45
ER -
TY - GEN
AB - Hippocampal GABAergic interneurons show diverse molecular and morphological properties. The functional significance of this diversity for information processing is poorly understood. Here we show that cholecystokinin (CCK)-expressing interneurons in rat dentate gyrus release GABA in a highly asynchronous manner, in contrast to parvalbumin (PV) interneurons. With a gamma-frequency burst of ten action potentials, the ratio of asynchronous to synchronous release is 3:1 in CCK interneurons but is 1:5 in parvalbumin interneurons. N-type channels trigger synchronous and asynchronous release in CCK interneuron synapses, whereas P/Q-type Ca(2+) channels mediate release at PV interneuron synapses. Effects of Ca(2+) chelators suggest that both a long-lasting presynaptic Ca(2+) transient and a large distance between Ca(2+) source and sensor of exocytosis contribute to the higher ratio of asynchronous to synchronous release in CCK interneuron synapses. Asynchronous release occurs at physiological temperature and with behaviorally relevant stimulation patterns, thus generating long-lasting inhibition in the brain.
AU - Hefft, Stefan
AU - Peter Jonas
ID - 3812
IS - 10
T2 - Nature Neuroscience
TI - Asynchronous GABA release generates long-lasting inhibition at a hippocampal interneuron-principal neuron synapse (Review)
VL - 8
ER -
TY - CONF
AB - In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it often suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of omega-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.
AU - Krishnendu Chatterjee
AU - Thomas Henzinger
AU - Jurdziński, Marcin
ID - 3892
TI - Games with secure equilibria
VL - 3657
ER -
TY - CONF
AB - We study infinite stochastic games played by two-players on a finite graph with goals specified by sets of infinite traces. The games are concurrent (each player simultaneously and independently chooses an action at each round), stochastic (the next state is determined by a probability distribution depending on the current state and the chosen actions), infinite (the game continues for an infinite number of rounds), nonzero-sum (the players' goals are not necessarily conflicting), and undiscounted. We show that if each player has an W-regular objective expressed as a paxity objective, then there exists an epsilon-Nash equilibrium, for every epsilon > 0. However, exact Nash equilibria need not exist. We study the complexity of finding values (payoff profile) of an epsilon-Nash equilibrium. We show that the values of an epsilon-Nash equilibrium in nonzero-sum concurrent parity games can be computed by solving the following two simpler problems: computing the values of zero-sum (the goals of the players axe strictly conflicting) concurrent parity games and computing epsilon-Nash equilibrium values of nonzero-sum concurrent games with reachability objectives. As a consequence we establish that values of an epsilon-Nash equilibrium can be computed in TFNP (total functional NP), and hence in EXPTIME.
AU - Krishnendu Chatterjee
ID - 3893
TI - Two-player nonzero-sum ω-regular games
VL - 3653
ER -
TY - CONF
AB - Temporal Logic Model Checking is one of the most potent tools for the verification of finite state systems. Computation Tree Logic (CTL) has gained popularity because unlike most other logics, CTL model checking of a single transition system can be achieved in polynomial time. However, in most real-life problems, specially in distributed and parallel systems, the system consist of a set of concurrent processes and the verification problem translates to model check the composition of the component processes. Since explicit composition leads to state explosion, verifying the system without actually composing the components is attractive, even for possibly restrictive class of systems. We show that the problem of compositional CTL model checking is PSPACE complete for the class of systems composed of components that are tree-like transition structure and do not interact among themselves. For the simplest forms of existential and universal CTL formulas model checking turns out to be NP complete and coNP complete, respectively. The results hold for both synchronous and asynchronous composition.
AU - Krishnendu Chatterjee
AU - Dasgupta, Pallab
AU - Chakrabarti, Partha P
ID - 3896
TI - Complexity of compositional model checking of computation tree logic on simple structures
VL - 3326
ER -