@article{2184, abstract = {Given topological spaces X,Y, a fundamental problem of algebraic topology is understanding the structure of all continuous maps X→ Y. We consider a computational version, where X,Y are given as finite simplicial complexes, and the goal is to compute [X,Y], that is, all homotopy classes of suchmaps.We solve this problem in the stable range, where for some d ≥ 2, we have dim X ≤ 2d-2 and Y is (d-1)-connected; in particular, Y can be the d-dimensional sphere Sd. The algorithm combines classical tools and ideas from homotopy theory (obstruction theory, Postnikov systems, and simplicial sets) with algorithmic tools from effective algebraic topology (locally effective simplicial sets and objects with effective homology). In contrast, [X,Y] is known to be uncomputable for general X,Y, since for X = S1 it includes a well known undecidable problem: testing triviality of the fundamental group of Y. In follow-up papers, the algorithm is shown to run in polynomial time for d fixed, and extended to other problems, such as the extension problem, where we are given a subspace A ⊂ X and a map A→ Y and ask whether it extends to a map X → Y, or computing the Z2-index-everything in the stable range. Outside the stable range, the extension problem is undecidable.}, author = {Čadek, Martin and Krcál, Marek and Matoušek, Jiří and Sergeraert, Francis and Vokřínek, Lukáš and Wagner, Uli}, journal = {Journal of the ACM}, number = {3}, publisher = {ACM}, title = {{Computing all maps into a sphere}}, doi = {10.1145/2597629}, volume = {61}, year = {2014}, } @article{2183, abstract = {We describe a simple adaptive network of coupled chaotic maps. The network reaches a stationary state (frozen topology) for all values of the coupling parameter, although the dynamics of the maps at the nodes of the network can be nontrivial. The structure of the network shows interesting hierarchical properties and in certain parameter regions the dynamics is polysynchronous: Nodes can be divided in differently synchronized classes but, contrary to cluster synchronization, nodes in the same class need not be connected to each other. These complicated synchrony patterns have been conjectured to play roles in systems biology and circuits. The adaptive system we study describes ways whereby this behavior can evolve from undifferentiated nodes.}, author = {Botella Soler, Vicente and Glendinning, Paul}, journal = {Physical Review E Statistical Nonlinear and Soft Matter Physics}, number = {6}, publisher = {American Institute of Physics}, title = {{Hierarchy and polysynchrony in an adaptive network }}, doi = {10.1103/PhysRevE.89.062809}, volume = {89}, year = {2014}, } @article{2186, abstract = {We prove the existence of scattering states for the defocusing cubic Gross-Pitaevskii (GP) hierarchy in ℝ3. Moreover, we show that an exponential energy growth condition commonly used in the well-posedness theory of the GP hierarchy is, in a specific sense, necessary. In fact, we prove that without the latter, there exist initial data for the focusing cubic GP hierarchy for which instantaneous blowup occurs.}, author = {Chen, Thomas and Hainzl, Christian and Pavlović, Nataša and Seiringer, Robert}, journal = {Letters in Mathematical Physics}, number = {7}, pages = {871 -- 891}, publisher = {Springer}, title = {{On the well-posedness and scattering for the Gross-Pitaevskii hierarchy via quantum de Finetti}}, doi = {10.1007/s11005-014-0693-2}, volume = {104}, year = {2014}, } @article{2187, abstract = {Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results.}, author = {Bloem, Roderick and Chatterjee, Krishnendu and Greimel, Karin and Henzinger, Thomas A and Hofferek, Georg and Jobstmann, Barbara and Könighofer, Bettina and Könighofer, Robert}, journal = {Acta Informatica}, number = {3-4}, pages = {193 -- 220}, publisher = {Springer}, title = {{Synthesizing robust systems}}, doi = {10.1007/s00236-013-0191-5}, volume = {51}, year = {2014}, } @article{2188, abstract = {Although plant and animal cells use a similar core mechanism to deliver proteins to the plasma membrane, their different lifestyle, body organization and specific cell structures resulted in the acquisition of regulatory mechanisms that vary in the two kingdoms. In particular, cell polarity regulators do not seem to be conserved, because genes encoding key components are absent in plant genomes. In plants, the broad knowledge on polarity derives from the study of auxin transporters, the PIN-FORMED proteins, in the model plant Arabidopsis thaliana. In animals, much information is provided from the study of polarity in epithelial cells that exhibit basolateral and luminal apical polarities, separated by tight junctions. In this review, we summarize the similarities and differences of the polarization mechanisms between plants and animals and survey the main genetic approaches that have been used to characterize new genes involved in polarity establishment in plants, including the frequently used forward and reverse genetics screens as well as a novel chemical genetics approach that is expected to overcome the limitation of classical genetics methods.}, author = {Kania, Urszula and Fendrych, Matyas and Friml, Jiřĺ}, journal = {Open Biology}, number = {APRIL}, publisher = {Royal Society}, title = {{Polar delivery in plants; commonalities and differences to animal epithelial cells}}, doi = {10.1098/rsob.140017}, volume = {4}, year = {2014}, } @inproceedings{2189, abstract = {En apprentissage automatique, nous parlons d'adaptation de domaine lorsque les données de test (cibles) et d'apprentissage (sources) sont générées selon différentes distributions. Nous devons donc développer des algorithmes de classification capables de s'adapter à une nouvelle distribution, pour laquelle aucune information sur les étiquettes n'est disponible. Nous attaquons cette problématique sous l'angle de l'approche PAC-Bayésienne qui se focalise sur l'apprentissage de modèles définis comme des votes de majorité sur un ensemble de fonctions. Dans ce contexte, nous introduisons PV-MinCq une version adaptative de l'algorithme (non adaptatif) MinCq. PV-MinCq suit le principe suivant. Nous transférons les étiquettes sources aux points cibles proches pour ensuite appliquer MinCq sur l'échantillon cible ``auto-étiqueté'' (justifié par une borne théorique). Plus précisément, nous définissons un auto-étiquetage non itératif qui se focalise dans les régions où les distributions marginales source et cible sont les plus similaires. Dans un second temps, nous étudions l'influence de notre auto-étiquetage pour en déduire une procédure de validation des hyperparamètres. Finalement, notre approche montre des résultats empiriques prometteurs.}, author = {Morvant, Emilie}, location = {Saint-Etienne, France}, pages = {49--58}, publisher = {Elsevier}, title = {{Adaptation de domaine de vote de majorité par auto-étiquetage non itératif}}, volume = {1}, year = {2014}, } @inproceedings{2190, abstract = {We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.}, author = {Esparza, Javier and Kretinsky, Jan}, pages = {192 -- 208}, publisher = {Springer}, title = {{From LTL to deterministic automata: A safraless compositional approach}}, doi = {10.1007/978-3-319-08867-9_13}, volume = {8559}, year = {2014}, } @article{2208, abstract = {We propose to detect quadrupole interactions of neutral ultracold atoms via their induced mean-field shift. We consider a Mott insulator state of spin-polarized atoms in a two-dimensional optical square lattice. The quadrupole moments of the atoms are aligned by an external magnetic field. As the alignment angle is varied, the mean-field shift shows a characteristic angular dependence, which constitutes the defining signature of the quadrupole interaction. For the 3P2 states of Yb and Sr atoms, we find a frequency shift of the order of tens of Hertz, which can be realistically detected in experiment with current technology. We compare our results to the mean-field shift of a spin-polarized quasi-two-dimensional Fermi gas in continuum. }, author = {Lahrz, Martin and Lemeshko, Mikhail and Sengstock, Klaus and Becker, Christoph and Mathey, Ludwig}, journal = {Physical Review A - Atomic, Molecular, and Optical Physics}, number = {4}, publisher = {American Physical Society}, title = {{Detecting quadrupole interactions in ultracold Fermi gases}}, doi = {10.1103/PhysRevA.89.043616}, volume = {89}, year = {2014}, } @article{2214, abstract = {A hallmark of immune cell trafficking is directional guidance via gradients of soluble or surface bound chemokines. Vascular endothelial cells produce, transport and deposit either their own chemokines or chemokines produced by the underlying stroma. Endothelial heparan sulfate (HS) was suggested to be a critical scaffold for these chemokine pools, but it is unclear how steep chemokine gradients are sustained between the lumenal and ablumenal aspects of blood vessels. Addressing this question by semi-quantitative immunostaining of HS moieties around blood vessels with a pan anti-HS IgM mAb, we found a striking HS enrichment in the basal lamina of resting and inflamed post capillary skin venules, as well as in high endothelial venules (HEVs) of lymph nodes. Staining of skin vessels with a glycocalyx probe further suggested that their lumenal glycocalyx contains much lower HS density than their basolateral extracellular matrix (ECM). This polarized HS pattern was observed also in isolated resting and inflamed microvascular dermal cells. Notably, progressive skin inflammation resulted in massive ECM deposition and in further HS enrichment around skin post capillary venules and their associated pericytes. Inflammation-dependent HS enrichment was not compromised in mice deficient in the main HS degrading enzyme, heparanase. Our results suggest that the blood vasculature patterns steep gradients of HS scaffolds between their lumenal and basolateral endothelial aspects, and that inflammatory processes can further enrich the HS content nearby inflamed vessels. We propose that chemokine gradients between the lumenal and ablumenal sides of vessels could be favored by these sharp HS scaffold gradients.}, author = {Stoler Barak, Liat and Moussion, Christine and Shezen, Elias and Hatzav, Miki and Sixt, Michael K and Alon, Ronen}, journal = {PLoS One}, number = {1}, publisher = {Public Library of Science}, title = {{Blood vessels pattern heparan sulfate gradients between their apical and basolateral aspects}}, doi = {10.1371/journal.pone.0085699}, volume = {9}, year = {2014}, } @article{2215, abstract = {Homologous recombination is crucial for genome stability and for genetic exchange. Although our knowledge of the principle steps in recombination and its machinery is well advanced, homology search, the critical step of exploring the genome for homologous sequences to enable recombination, has remained mostly enigmatic. However, recent methodological advances have provided considerable new insights into this fundamental step in recombination that can be integrated into a mechanistic model. These advances emphasize the importance of genomic proximity and nuclear organization for homology search and the critical role of homology search mediators in this process. They also aid our understanding of how homology search might lead to unwanted and potentially disease-promoting recombination events.}, author = {Renkawitz, Jörg and Lademann, Claudio and Jentsch, Stefan}, journal = {Nature Reviews Molecular Cell Biology}, number = {6}, pages = {369 -- 383}, publisher = {Nature Publishing Group}, title = {{Mechanisms and principles of homology search during recombination}}, doi = {10.1038/nrm3805}, volume = {15}, year = {2014}, } @article{2223, abstract = {Correct positioning of membrane proteins is an essential process in eukaryotic organisms. The plant hormone auxin is distributed through intercellular transport and triggers various cellular responses. Auxin transporters of the PIN-FORMED (PIN) family localize asymmetrically at the plasma membrane (PM) and mediate the directional transport of auxin between cells. A fungal toxin, brefeldin A (BFA), inhibits a subset of guanine nucleotide exchange factors for ADP-ribosylation factor small GTPases (ARF GEFs) including GNOM, which plays a major role in localization of PIN1 predominantly to the basal side of the PM. The Arabidopsis genome encodes 19 ARF-related putative GTPases. However, ARF components involved in PIN1 localization have been genetically poorly defined. Using a fluorescence imaging-based forward genetic approach, we identified an Arabidopsis mutant, bfa-visualized exocytic trafficking defective1 (bex1), in which PM localization of PIN1-green fluorescent protein (GFP) as well as development is hypersensitive to BFA. We found that in bex1 a member of the ARF1 gene family, ARF1A1C, was mutated. ARF1A1C localizes to the trans-Golgi network/early endosome and Golgi apparatus, acts synergistically to BEN1/MIN7 ARF GEF and is important for PIN recycling to the PM. Consistent with the developmental importance of PIN proteins, functional interference with ARF1 resulted in an impaired auxin response gradient and various developmental defects including embryonic patterning defects and growth arrest. Our results show that ARF1A1C is essential for recycling of PIN auxin transporters and for various auxin-dependent developmental processes.}, author = {Tanaka, Hirokazu and Nodzyński, Tomasz and Kitakura, Saeko and Feraru, Mugurel and Sasabe, Michiko and Ishikawa, Tomomi and Kleine Vehn, Jürgen and Kakimoto, Tatsuo and Friml, Jirí}, issn = {00320781}, journal = {Plant and Cell Physiology}, number = {4}, pages = {737 -- 749}, publisher = {Oxford University Press}, title = {{BEX1/ARF1A1C is required for BFA-sensitive recycling of PIN auxin transporters and auxin-mediated development in arabidopsis}}, doi = {10.1093/pcp/pct196}, volume = {55}, year = {2014}, } @article{2225, abstract = {We consider sample covariance matrices of the form X∗X, where X is an M×N matrix with independent random entries. We prove the isotropic local Marchenko-Pastur law, i.e. we prove that the resolvent (X∗X−z)−1 converges to a multiple of the identity in the sense of quadratic forms. More precisely, we establish sharp high-probability bounds on the quantity ⟨v,(X∗X−z)−1w⟩−⟨v,w⟩m(z), where m is the Stieltjes transform of the Marchenko-Pastur law and v,w∈CN. We require the logarithms of the dimensions M and N to be comparable. Our result holds down to scales Iz≥N−1+ε and throughout the entire spectrum away from 0. We also prove analogous results for generalized Wigner matrices. }, author = {Bloemendal, Alex and Erdös, László and Knowles, Antti and Yau, Horng and Yin, Jun}, issn = {10836489}, journal = {Electronic Journal of Probability}, publisher = {Institute of Mathematical Statistics}, title = {{Isotropic local laws for sample covariance and generalized Wigner matrices}}, doi = {10.1214/EJP.v19-3054}, volume = {19}, year = {2014}, } @article{2222, abstract = {Leaf venation develops complex patterns in angiosperms, but the mechanism underlying this process is largely unknown. To elucidate the molecular mechanisms governing vein pattern formation, we previously isolated vascular network defective (van) mutants that displayed venation discontinuities. Here, we report the phenotypic analysis of van4 mutants, and we identify and characterize the VAN4 gene. Detailed phenotypic analysis shows that van4 mutants are defective in procambium cell differentiation and subsequent vascular cell differentiation. Reduced shoot and root cell growth is observed in van4 mutants, suggesting that VAN4 function is important for cell growth and the establishment of venation continuity. Consistent with these phenotypes, the VAN4 gene is strongly expressed in vascular and meristematic cells. VAN4 encodes a putative TRS120, which is a known guanine nucleotide exchange factor (GEF) for Rab GTPase involved in regulating vesicle transport, and a known tethering factor that determines the specificity of membrane fusion. VAN4 protein localizes at the trans-Golgi network/early endosome (TGN/EE). Aberrant recycling of the auxin efflux carrier PIN proteins is observed in van4 mutants. These results suggest that VAN4-mediated exocytosis at the TGN plays important roles in plant vascular development and cell growth in shoot and root. Our identification of VAN4 as a putative TRS120 shows that Rab GTPases are crucial (in addition to ARF GTPases) for continuous vascular development, and provides further evidence for the importance of vesicle transport in leaf vascular formation.}, author = {Naramoto, Satoshi and Nodzyński, Tomasz and Dainobu, Tomoko and Takatsuka, Hirotomo and Okada, Teruyo and Friml, Jirí and Fukuda, Hiroo}, issn = {00320781}, journal = {Plant and Cell Physiology}, number = {4}, pages = {750 -- 763}, publisher = {Oxford University Press}, title = {{VAN4 encodes a putative TRS120 that is required for normal cell growth and vein development in arabidopsis}}, doi = {10.1093/pcp/pcu012}, volume = {55}, year = {2014}, } @article{2224, abstract = {This work investigates the transition between different traveling helical waves (spirals, SPIs) in the setup of differentially independent rotating cylinders. We use direct numerical simulations to consider an infinite long and periodic Taylor-Couette apparatus with fixed axial periodicity length. We find so-called mixed-cross-spirals (MCSs), that can be seen as nonlinear superpositions of SPIs, to establish stable footbridges connecting SPI states. While bridging the bifurcation branches of SPIs, the corresponding contributions within the MCS vary continuously with the control parameters. Here discussed MCSs presenting footbridge solutions start and end in different SPI branches. Therefore they differ significantly from the already known MCSs that present bypass solutions (Altmeyer and Hoffmann 2010 New J. Phys. 12 113035). The latter start and end in the same SPI branch, while they always bifurcate out of those SPI branches with the larger mode amplitude. Meanwhile, these only appear within the coexisting region of both SPIs. In contrast, the footbridge solutions can also bifurcate out of the minor SPI contribution. We also find they exist in regions where only one of the SPIs contributions exists. In addition, MCS as footbridge solution can appear either stable or unstable. The latter detected transient solutions offer similar spatio-temporal characteristics to the flow establishing stable footbridges. Such transition processes are interesting for pattern-forming systems in general because they accomplish transitions between traveling waves of different azimuthal wave numbers and have not been described in the literature yet.}, author = {Altmeyer, Sebastian}, issn = {01695983}, journal = {Fluid Dynamics Research}, number = {2}, publisher = {IOP Publishing Ltd.}, title = {{On secondary instabilities generating footbridges between spiral vortex flow}}, doi = {10.1088/0169-5983/46/2/025503}, volume = {46}, year = {2014}, } @inproceedings{2219, abstract = {Recently, Döttling et al. (ASIACRYPT 2012) proposed the first chosen-ciphertext (IND-CCA) secure public-key encryption scheme from the learning parity with noise (LPN) assumption. In this work we give an alternative scheme which is conceptually simpler and more efficient. At the core of our construction is a trapdoor technique originally proposed for lattices by Micciancio and Peikert (EUROCRYPT 2012), which we adapt to the LPN setting. The main technical tool is a new double-trapdoor mechanism, together with a trapdoor switching lemma based on a computational variant of the leftover hash lemma.}, author = {Kiltz, Eike and Masny, Daniel and Pietrzak, Krzysztof Z}, isbn = {978-364254630-3}, pages = {1 -- 18}, publisher = {Springer}, title = {{Simple chosen-ciphertext security from low noise LPN}}, doi = {10.1007/978-3-642-54631-0_1}, volume = {8383}, year = {2014}, } @article{2220, abstract = {In this issue of Chemistry & Biology, Cokol and colleagues report a systematic study of drug interactions between antifungal compounds. Suppressive drug interactions occur more frequently than previously realized and come in different flavors with interesting implications.}, author = {De Vos, Marjon and Bollenbach, Mark Tobias}, issn = {10745521}, journal = {Chemistry and Biology}, number = {4}, pages = {439 -- 440}, publisher = {Cell Press}, title = {{Suppressive drug interactions between antifungals}}, doi = {10.1016/j.chembiol.2014.04.004}, volume = {21}, year = {2014}, } @article{2233, abstract = { A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, valuing a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by λi, where the discount factor λ is a fixed rational number greater than 1. The value of a word is the minimal value of the automaton runs on it. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, reflecting the assumption that earlier weights are more important than later weights. Unfortunately, determinization of NDAs, which is often essential in formal verification, is, in general, not possible. We provide positive news, showing that every NDA with an integral discount factor is determinizable. We complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: for every nonintegral rational discount factor λ, there is a nondeterminizable λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. For general NDAs, we look into approximate determinization, which is always possible as the influence of a word's suffix decays. We show that the naive approach, of unfolding the automaton computations up to a sufficient level, is doubly exponential in the discount factor. We provide an alternative construction for approximate determinization, which is singly exponential in the discount factor, in the precision, and in the number of states. We also prove matching lower bounds, showing that the exponential dependency on each of these three parameters cannot be avoided. All our results hold equally for automata over finite words and for automata over infinite words. }, author = {Boker, Udi and Henzinger, Thomas A}, issn = {18605974}, journal = {Logical Methods in Computer Science}, number = {1}, publisher = {International Federation of Computational Logic}, title = {{Exact and approximate determinization of discounted-sum automata}}, doi = {10.2168/LMCS-10(1:10)2014}, volume = {10}, year = {2014}, } @article{2230, abstract = {Intracellular electrophysiological recordings provide crucial insights into elementary neuronal signals such as action potentials and synaptic currents. Analyzing and interpreting these signals is essential for a quantitative understanding of neuronal information processing, and requires both fast data visualization and ready access to complex analysis routines. To achieve this goal, we have developed Stimfit, a free software package for cellular neurophysiology with a Python scripting interface and a built-in Python shell. The program supports most standard file formats for cellular neurophysiology and other biomedical signals through the Biosig library. To quantify and interpret the activity of single neurons and communication between neurons, the program includes algorithms to characterize the kinetics of presynaptic action potentials and postsynaptic currents, estimate latencies between pre- and postsynaptic events, and detect spontaneously occurring events. We validate and benchmark these algorithms, give estimation errors, and provide sample use cases, showing that Stimfit represents an efficient, accessible and extensible way to accurately analyze and interpret neuronal signals.}, author = {Guzmán, José and Schlögl, Alois and Schmidt Hieber, Christoph}, issn = {16625196}, journal = {Frontiers in Neuroinformatics}, number = {FEB}, publisher = {Frontiers Research Foundation}, title = {{Stimfit: Quantifying electrophysiological data with Python}}, doi = {10.3389/fninf.2014.00016}, volume = {8}, year = {2014}, } @article{2228, abstract = {Fast-spiking, parvalbumin-expressing GABAergic interneurons, a large proportion of which are basket cells (BCs), have a key role in feedforward and feedback inhibition, gamma oscillations and complex information processing. For these functions, fast propagation of action potentials (APs) from the soma to the presynaptic terminals is important. However, the functional properties of interneuron axons remain elusive. We examined interneuron axons by confocally targeted subcellular patch-clamp recording in rat hippocampal slices. APs were initiated in the proximal axon ∼20 μm from the soma and propagated to the distal axon with high reliability and speed. Subcellular mapping revealed a stepwise increase of Na^+ conductance density from the soma to the proximal axon, followed by a further gradual increase in the distal axon. Active cable modeling and experiments with partial channel block revealed that low axonal Na^+ conductance density was sufficient for reliability, but high Na^+ density was necessary for both speed of propagation and fast-spiking AP phenotype. Our results suggest that a supercritical density of Na^+ channels compensates for the morphological properties of interneuron axons (small segmental diameter, extensive branching and high bouton density), ensuring fast AP propagation and high-frequency repetitive firing.}, author = {Hu, Hua and Jonas, Peter M}, issn = {10976256}, journal = {Nature Neuroscience}, number = {5}, pages = {686--693}, publisher = {Nature Publishing Group}, title = {{A supercritical density of Na^+ channels ensures fast signaling in GABAergic interneuron axons}}, doi = {10.1038/nn.3678}, volume = {17}, year = {2014}, } @article{2229, abstract = {The distance between Ca^2+ channels and release sensors determines the speed and efficacy of synaptic transmission. Tight "nanodomain" channel-sensor coupling initiates transmitter release at synapses in the mature brain, whereas loose "microdomain" coupling appears restricted to early developmental stages. To probe the coupling configuration at a plastic synapse in the mature central nervous system, we performed paired recordings between mossy fiber terminals and CA3 pyramidal neurons in rat hippocampus. Millimolar concentrations of both the fast Ca^2+ chelator BAPTA [1,2-bis(2-aminophenoxy)ethane- N,N, N′,N′-tetraacetic acid] and the slow chelator EGTA efficiently suppressed transmitter release, indicating loose coupling between Ca^2+ channels and release sensors. Loose coupling enabled the control of initial release probability by fast endogenous Ca^2+ buffers and the generation of facilitation by buffer saturation. Thus, loose coupling provides the molecular framework for presynaptic plasticity.}, author = {Vyleta, Nicholas and Jonas, Peter M}, issn = {00368075}, journal = {Science}, number = {6171}, pages = {665 -- 670}, publisher = {American Association for the Advancement of Science}, title = {{Loose coupling between Ca^2+ channels and release sensors at a plastic hippocampal synapse}}, doi = {10.1126/science.1244811}, volume = {343}, year = {2014}, } @article{2232, abstract = {The purpose of this contribution is to summarize and discuss recent advances regarding the onset of turbulence in shear flows. The absence of a clear-cut instability mechanism, the spatio-temporal intermittent character and extremely long lived transients are some of the major difficulties encountered in these flows and have hindered progress towards understanding the transition process. We will show for the case of pipe flow that concepts from nonlinear dynamics and statistical physics can help to explain the onset of turbulence. In particular, the turbulent structures (puffs) observed close to onset are spatially localized chaotic transients and their lifetimes increase super-exponentially with Reynolds number. At the same time fluctuations of individual turbulent puffs can (although very rarely) lead to the nucleation of new puffs. The competition between these two stochastic processes gives rise to a non-equilibrium phase transition where turbulence changes from a super-transient to a sustained state.}, author = {Song, Baofang and Hof, Björn}, issn = {17425468}, journal = {Journal of Statistical Mechanics Theory and Experiment}, number = {2}, publisher = {IOP Publishing}, title = {{Deterministic and stochastic aspects of the transition to turbulence}}, doi = {10.1088/1742-5468/2014/02/P02001}, volume = {2014}, year = {2014}, } @article{2231, abstract = {Based on the measurements of noise in gene expression performed during the past decade, it has become customary to think of gene regulation in terms of a two-state model, where the promoter of a gene can stochastically switch between an ON and an OFF state. As experiments are becoming increasingly precise and the deviations from the two-state model start to be observable, we ask about the experimental signatures of complex multistate promoters, as well as the functional consequences of this additional complexity. In detail, we i), extend the calculations for noise in gene expression to promoters described by state transition diagrams with multiple states, ii), systematically compute the experimentally accessible noise characteristics for these complex promoters, and iii), use information theory to evaluate the channel capacities of complex promoter architectures and compare them with the baseline provided by the two-state model. We find that adding internal states to the promoter generically decreases channel capacity, except in certain cases, three of which (cooperativity, dual-role regulation, promoter cycling) we analyze in detail.}, author = {Rieckh, Georg and Tkacik, Gasper}, issn = {00063495}, journal = {Biophysical Journal}, number = {5}, pages = {1194 -- 1204}, publisher = {Biophysical Society}, title = {{Noise and information transmission in promoters with multiple internal states}}, doi = {10.1016/j.bpj.2014.01.014}, volume = {106}, year = {2014}, } @article{2226, abstract = {Coriolis force effects on shear flows are important in geophysical and astrophysical contexts. We report a study on the linear stability and the transient energy growth of the plane Couette flow with system rotation perpendicular to the shear direction. External rotation causes linear instability. At small rotation rates, the onset of linear instability scales inversely with the rotation rate and the optimal transient growth in the linearly stable region is slightly enhanced ∼Re2. The corresponding optimal initial perturbations are characterized by roll structures inclined in the streamwise direction and are twisted under external rotation. At large rotation rates, the transient growth is significantly inhibited and hence linear stability analysis is a reliable indicator for instability.}, author = {Shi, Liang and Hof, Björn and Tilgner, Andreas}, issn = {15393755}, journal = {Physical Review E Statistical Nonlinear and Soft Matter Physics}, number = {1}, publisher = {American Institute of Physics}, title = {{Transient growth of Ekman-Couette flow}}, doi = {10.1103/PhysRevE.89.013001}, volume = {89}, year = {2014}, } @article{2227, abstract = {The Balkan Peninsula, characterized by high rates of endemism, is recognised as one of the most diverse and species-rich areas of Europe. However, little is known about the origin of Balkan endemics. The present study addresses the phylogenetic position of the Balkan endemic Ranunculus wettsteinii, as well as its taxonomic status and relationship with the widespread R. parnassiifolius, based on nuclear DNA (internal transcribed spacer, ITS) and plastid regions (rpl32-trnL, rps16-trnQ, trnK-matK and ycf6-psbM). Maximum parsimony and Bayesian inference analyses revealed a well-supported clade formed by accessions of R. wettsteinii. Furthermore, our phylogenetic and network analyses supported previous hypotheses of a likely allopolyploid origin for R. wettsteinii between R. montenegrinus and R. parnassiifolius, with the latter as the maternal parent.}, author = {Cires Rodriguez, Eduardo and Baltisberger, Matthias and Cuesta, Candela and Vargas, Pablo and Prieto, José}, issn = {14396092}, journal = {Organisms Diversity and Evolution}, number = {1}, pages = {1 -- 10}, publisher = {Springer}, title = {{Allopolyploid origin of the Balkan endemic Ranunculus wettsteinii (Ranunculaceae) inferred from nuclear and plastid DNA sequences}}, doi = {10.1007/s13127-013-0150-6}, volume = {14}, year = {2014}, } @article{2234, abstract = {We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with κ limit-average functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the case of one limit-average function, both randomization and memory are necessary for strategies even for ε-approximation, and that finite-memory randomized strategies are sufficient for achieving Pareto optimal values. Under the satisfaction objective, in contrast to the case of one limit-average function, infinite memory is necessary for strategies achieving a specific value (i.e. randomized finite-memory strategies are not sufficient), whereas memoryless randomized strategies are sufficient for ε-approximation, for all ε > 0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be ε-approximated in time polynomial in the size of the MDP and 1/ε, and exponential in the number of limit-average functions, for all ε > 0. Our analysis also reveals flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, corrects the flaws, and allows us to obtain improved results.}, author = {Brázdil, Tomáš and Brožek, Václav and Chatterjee, Krishnendu and Forejt, Vojtěch and Kučera, Antonín}, issn = {18605974}, journal = {Logical Methods in Computer Science}, number = {1}, publisher = {International Federation of Computational Logic}, title = {{Markov decision processes with multiple long-run average objectives}}, doi = {10.2168/LMCS-10(1:13)2014}, volume = {10}, year = {2014}, } @inproceedings{2236, abstract = {Consider a joint distribution (X,A) on a set. We show that for any family of distinguishers, there exists a simulator such that 1 no function in can distinguish (X,A) from (X,h(X)) with advantage ε, 2 h is only O(2 3ℓ ε -2) times less efficient than the functions in. For the most interesting settings of the parameters (in particular, the cryptographic case where X has superlogarithmic min-entropy, ε > 0 is negligible and consists of circuits of polynomial size), we can make the simulator h deterministic. As an illustrative application of our theorem, we give a new security proof for the leakage-resilient stream-cipher from Eurocrypt'09. Our proof is simpler and quantitatively much better than the original proof using the dense model theorem, giving meaningful security guarantees if instantiated with a standard blockcipher like AES. Subsequent to this work, Chung, Lui and Pass gave an interactive variant of our main theorem, and used it to investigate weak notions of Zero-Knowledge. Vadhan and Zheng give a more constructive version of our theorem using their new uniform min-max theorem.}, author = {Jetchev, Dimitar and Pietrzak, Krzysztof Z}, editor = {Lindell, Yehuda}, isbn = {978-364254241-1}, location = {San Diego, USA}, pages = {566 -- 590}, publisher = {Springer}, title = {{How to fake auxiliary input}}, doi = {10.1007/978-3-642-54242-8_24}, volume = {8349}, year = {2014}, } @article{2240, abstract = {Clathrin-mediated endocytosis is the major mechanism for eukaryotic plasma membrane-based proteome turn-over. In plants, clathrin-mediated endocytosis is essential for physiology and development, but the identification and organization of the machinery operating this process remains largely obscure. Here, we identified an eight-core-component protein complex, the TPLATE complex, essential for plant growth via its role as major adaptor module for clathrin-mediated endocytosis. This complex consists of evolutionarily unique proteins that associate closely with core endocytic elements. The TPLATE complex is recruited as dynamic foci at the plasma membrane preceding recruitment of adaptor protein complex 2, clathrin, and dynamin-related proteins. Reduced function of different complex components severely impaired internalization of assorted endocytic cargoes, demonstrating its pivotal role in clathrin-mediated endocytosis. Taken together, the TPLATE complex is an early endocytic module representing a unique evolutionary plant adaptation of the canonical eukaryotic pathway for clathrin-mediated endocytosis.}, author = {Gadeyne, Astrid and Sánchez Rodríguez, Clara and Vanneste, Steffen and Di Rubbo, Simone and Zauber, Henrik and Vanneste, Kevin and Van Leene, Jelle and De Winne, Nancy and Eeckhout, Dominique and Persiau, Geert and Van De Slijke, Eveline and Cannoot, Bernard and Vercruysse, Leen and Mayers, Jonathan and Adamowski, Maciek and Kania, Urszula and Ehrlich, Matthias and Schweighofer, Alois and Ketelaar, Tijs and Maere, Steven and Bednarek, Sebastian and Friml, Jirí and Gevaert, Kris and Witters, Erwin and Russinova, Eugenia and Persson, Staffan and De Jaeger, Geert and Van Damme, Daniël}, issn = {00928674}, journal = {Cell}, number = {4}, pages = {691 -- 704}, publisher = {Cell Press}, title = {{The TPLATE adaptor complex drives clathrin-mediated endocytosis in plants}}, doi = {10.1016/j.cell.2014.01.039}, volume = {156}, year = {2014}, } @inproceedings{2239, abstract = {The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce battery transition systems. In this model, a battery is viewed as consisting of two parts-the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank. Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the !-regular modelchecking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots.}, author = {Boker, Udi and Henzinger, Thomas A and Radhakrishna, Arjun}, isbn = {978-145032544-8}, location = {San Diego, USA}, number = {1}, pages = {595 -- 606}, publisher = {ACM}, title = {{Battery transition systems}}, doi = {10.1145/2535838.2535875}, volume = {49}, year = {2014}, } @article{2235, abstract = {Emerging infectious diseases (EIDs) pose a risk to human welfare, both directly and indirectly, by affecting managed livestock and wildlife that provide valuable resources and ecosystem services, such as the pollination of crops. Honeybees (Apis mellifera), the prevailing managed insect crop pollinator, suffer from a range of emerging and exotic high-impact pathogens, and population maintenance requires active management by beekeepers to control them. Wild pollinators such as bumblebees (Bombus spp.) are in global decline, one cause of which may be pathogen spillover from managed pollinators like honeybees or commercial colonies of bumblebees. Here we use a combination of infection experiments and landscape-scale field data to show that honeybee EIDs are indeed widespread infectious agents within the pollinator assemblage. The prevalence of deformed wing virus (DWV) and the exotic parasite Nosema ceranae in honeybees and bumblebees is linked; as honeybees have higher DWV prevalence, and sympatric bumblebees and honeybees are infected by the same DWV strains, Apis is the likely source of at least one major EID in wild pollinators. Lessons learned from vertebrates highlight the need for increased pathogen control in managed bee species to maintain wild pollinators, as declines in native pollinators may be caused by interspecies pathogen transmission originating from managed pollinators.}, author = {Fürst, Matthias and Mcmahon, Dino and Osborne, Juliet and Paxton, Robert and Brown, Mark}, issn = {00280836}, journal = {Nature}, number = {7488}, pages = {364 -- 366}, publisher = {Nature Publishing Group}, title = {{Disease associations between honeybees and bumblebees as a threat to wild pollinators}}, doi = {10.1038/nature12977}, volume = {506}, year = {2014}, } @article{2241, abstract = {The brain demands high-energy supply and obstruction of blood flow causes rapid deterioration of the healthiness of brain cells. Two major events occur upon ischemia: acidosis and liberation of excess glutamate, which leads to excitotoxicity. However, cellular source of glutamate and its release mechanism upon ischemia remained unknown. Here we show a causal relationship between glial acidosis and neuronal excitotoxicity. As the major cation that flows through channelrhodopsin-2 (ChR2) is proton, this could be regarded as an optogenetic tool for instant intracellular acidification. Optical activation of ChR2 expressed in glial cells led to glial acidification and to release of glutamate. On the other hand, glial alkalization via optogenetic activation of a proton pump, archaerhodopsin (ArchT), led to cessation of glutamate release and to the relief of ischemic brain damage in vivo. Our results suggest that controlling glial pH may be an effective therapeutic strategy for intervention of ischemic brain damage.}, author = {Beppu, Kaoru and Sasaki, Takuya and Tanaka, Kenji and Yamanaka, Akihiro and Fukazawa, Yugo and Shigemoto, Ryuichi and Matsui, Ko}, issn = {08966273}, journal = {Neuron}, number = {2}, pages = {314 -- 320}, publisher = {Elsevier}, title = {{Optogenetic countering of glial acidosis suppresses glial glutamate release and ischemic brain damage}}, doi = {10.1016/j.neuron.2013.11.011}, volume = {81}, year = {2014}, } @inbook{2245, abstract = {Exogenous application of biologically important molecules for plant growth promotion and/or regulation is very common both in plant research and horticulture. Plant hormones such as auxins and cytokinins are classes of compounds which are often applied exogenously. Nevertheless, plants possess a well-established machinery to regulate the active pool of exogenously applied compounds by converting them to metabolites and conjugates. Consequently, it is often very useful to know the in vivo status of applied compounds to connect them with some of the regulatory events in plant developmental processes. The in vivo status of applied compounds can be measured by incubating plants with radiolabeled compounds, followed by extraction, purification, and HPLC metabolic profiling of plant extracts. Recently we have used this method to characterize the intracellularly localized PIN protein, PIN5. Here we explain the method in detail, with a focus on general application. }, author = {Simon, Sibu and Skůpa, Petr and Dobrev, Petre and Petrášek, Jan and Zažímalová, Eva and Friml, Jirí}, booktitle = {Plant Chemical Genomics}, editor = {Hicks, Glenn and Robert, Stéphanie}, issn = {10643745}, pages = {255 -- 264}, publisher = {Springer}, title = {{Analyzing the in vivo status of exogenously applied auxins: A HPLC-based method to characterize the intracellularly localized auxin transporters}}, doi = {10.1007/978-1-62703-592-7_23}, volume = {1056}, year = {2014}, } @article{2246, abstract = {Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth. }, author = {Grinshpun, Andrey and Phalitnonkiat, Pakawat and Rubin, Sasha and Tarfulea, Andrei}, issn = {03043975}, journal = {Theoretical Computer Science}, pages = {73 -- 91}, publisher = {Elsevier}, title = {{Alternating traps in Muller and parity games}}, doi = {10.1016/j.tcs.2013.11.032}, volume = {521}, year = {2014}, } @article{2242, abstract = {MicroRNAs (miRNAs) are small RNAs that play important regulatory roles in many cellular pathways. MiRNAs associate with members of the Argonaute protein family and bind to partially complementary sequences on mRNAs and induce translational repression or mRNA decay. Using deep sequencing and Northern blotting, we characterized miRNA expression in wild type and miR-155-deficient dendritic cells (DCs) and macrophages. Analysis of different stimuli (LPS, LDL, eLDL, oxLDL) reveals a direct influence of miR-155 on the expression levels of other miRNAs. For example, miR-455 is negatively regulated in miR-155-deficient cells possibly due to inhibition of the transcription factor C/EBPbeta by miR-155. Based on our comprehensive data sets, we propose a model of hierarchical miRNA expression dominated by miR-155 in DCs and macrophages.}, author = {Dueck, Anne and Eichner, Alexander and Sixt, Michael K and Meister, Gunter}, issn = {00145793}, journal = {FEBS Letters}, number = {4}, pages = {632 -- 640}, publisher = {Elsevier}, title = {{A miR-155-dependent microRNA hierarchy in dendritic cell maturation and macrophage activation}}, doi = {10.1016/j.febslet.2014.01.009}, volume = {588}, year = {2014}, } @article{2250, abstract = {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.}, author = {Kuchibhatla, Durga and Sherman, Westley and Chung, Betty and Cook, Shelley and Schneider, Georg and Eisenhaber, Birgit and Karlin, David}, issn = {0022538X}, journal = {Journal of Virology}, number = {1}, pages = {10 -- 20}, publisher = {ASM}, title = {{Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently "orphan" viral proteins}}, doi = {10.1128/JVI.02595-13}, volume = {88}, year = {2014}, } @article{2254, abstract = {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.}, author = {Pernia-Andrade, Alejandro and Jonas, Peter M}, issn = {08966273}, journal = {Neuron}, number = {1}, pages = {140 -- 152}, publisher = {Elsevier}, title = {{Theta-gamma-modulated synaptic currents in hippocampal granule cells in vivo define a mechanism for network oscillations}}, doi = {10.1016/j.neuron.2013.09.046}, volume = {81}, year = {2014}, } @article{2251, abstract = {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.}, author = {Csicsvari, Jozsef L and Dupret, David}, issn = {09628436}, journal = {Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences}, number = {1635}, publisher = {Royal Society, The}, title = {{Sharp wave/ripple network oscillations and learning-associated hippocampal maps}}, doi = {10.1098/rstb.2012.0528}, volume = {369}, year = {2014}, } @article{2253, abstract = {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.}, author = {Bailly, Aurélien and Wang, Bangjun and Zwiewka, Marta and Pollmann, Stephan and Schenck, Daniel and Lüthen, Hartwig and Schulz, Alexander and Friml, Jirí and Geisler, Markus}, issn = {09607412}, journal = {Plant Journal}, number = {1}, pages = {108 -- 118}, publisher = {Wiley-Blackwell}, title = {{Expression of TWISTED DWARF1 lacking its in-plane membrane anchor leads to increased cell elongation and hypermorphic growth}}, doi = {10.1111/tpj.12369}, volume = {77}, year = {2014}, } @article{2248, abstract = {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.}, author = {Capek, Daniel and Metscher, Brian and Müller, Gerd}, issn = {15525007}, journal = {Journal of Experimental Zoology Part B: Molecular and Developmental Evolution}, number = {1}, pages = {1 -- 12}, publisher = {Wiley-Blackwell}, title = {{Thumbs down: A molecular-morphogenetic approach to avian digit homology}}, doi = {10.1002/jez.b.22545}, volume = {322}, year = {2014}, } @article{2249, abstract = {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.}, author = {Chen, Yani and Aung, Kyaw and Rolčík, Jakub and Walicki, Kathryn and Friml, Jirí and Brandizzí, Federica}, issn = {09607412}, journal = {Plant Journal}, number = {1}, pages = {97 -- 107}, publisher = {Wiley-Blackwell}, title = {{Inter-regulation of the unfolded protein response and auxin signaling}}, doi = {10.1111/tpj.12373}, volume = {77}, year = {2014}, } @article{2252, abstract = {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.}, author = {Phadke, Sujal and Paixao, Tiago and Pham, Tuan and Pham, Stephanie and Zufall, Rebecca}, issn = {00221503}, journal = {Journal of Heredity}, number = {1}, pages = {130 -- 135}, publisher = {Oxford University Press}, title = {{Genetic background alters dominance relationships between mat alleles in the ciliate Tetrahymena Thermophila}}, doi = {10.1093/jhered/est063}, volume = {105}, year = {2014}, } @article{2261, abstract = {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.}, author = {Zhu, Fangfang and Gamboa, Matthew and Farruggio, Alfonso and Hippenmeyer, Simon and Tasic, Bosiljka and Schüle, Birgitt and Chen Tsai, Yanru and Calos, Michele}, journal = {Nucleic Acids Research}, number = {5}, publisher = {Oxford University Press}, title = {{DICE, an efficient system for iterative genomic editing in human pluripotent stem cells}}, doi = {10.1093/nar/gkt1290}, volume = {42}, year = {2014}, } @inbook{2265, abstract = {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.}, author = {Hippenmeyer, Simon}, booktitle = { Cellular and Molecular Control of Neuronal Migration}, editor = {Nguyen, Laurent}, pages = {1 -- 24}, publisher = {Springer}, title = {{Molecular pathways controlling the sequential steps of cortical projection neuron migration}}, doi = {10.1007/978-94-007-7687-6_1}, volume = {800}, year = {2014}, } @inproceedings{2275, abstract = {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. }, author = {Olsson, Carl and Ulen, Johannes and Boykov, Yuri and Kolmogorov, Vladimir}, location = {Sydney, Australia}, pages = {2936 -- 2943}, publisher = {IEEE}, title = {{Partial enumeration and curvature regularization}}, doi = {10.1109/ICCV.2013.365}, year = {2014}, } @article{2285, abstract = {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.}, author = {Hosp, Jonas and Strüber, Michael and Yanagawa, Yuchio and Obata, Kunihiko and Vida, Imre and Jonas, Peter M and Bartos, Marlene}, journal = {Hippocampus}, number = {2}, pages = {189 -- 203}, publisher = {Wiley-Blackwell}, title = {{Morpho-physiological criteria divide dentate gyrus interneurons into classes}}, doi = {10.1002/hipo.22214}, volume = {23}, year = {2014}, } @article{2407, abstract = {Two definitions of the effective mass of a particle interacting with a quantum field, such as a polaron, are considered and shown to be equal in models similar to the Fröhlich polaron model. These are: 1. the mass defined by the low momentum energy E(P)≈E(0)+P2/2 M of the translation invariant system constrained to have momentum P and 2. the mass M of a simple particle in an arbitrary slowly varying external potential, V, described by the nonrelativistic Schrödinger equation, whose ground state energy equals that of the combined particle/field system in a bound state in the same V.}, author = {Lieb, Élliott and Seiringer, Robert}, journal = {Journal of Statistical Physics}, number = {1-2}, pages = {51 -- 57}, publisher = {Springer}, title = {{Equivalence of two definitions of the effective mass of a polaron}}, doi = {10.1007/s10955-013-0791-z}, volume = {154}, year = {2014}, } @article{248, abstract = {For any pencil of conics or higher-dimensional quadrics over ℚ, with all degenerate fibres defined over ℚ, we show that the Brauer–Manin obstruction controls weak approximation. The proof is based on the Hasse principle and weak approximation for some special intersections of quadrics over ℚ, which is a consequence of recent advances in additive combinatorics.}, author = {Timothy Browning and Matthiesen, Lilian and Skorobogatov, Alexei N}, journal = {Annals of Mathematics}, number = {1}, pages = {381 -- 402}, publisher = {John Hopkins University Press}, title = {{Rational points on pencils of conics and quadrics with many degenerate fibres}}, doi = {https://doi.org/10.4007/annals.2014.180.1.8}, volume = {180}, year = {2014}, } @article{249, abstract = {A version of the Hardy-Littlewood circle method is developed for number fields K/ℚ and is used to show that nonsingular projective cubic hypersurfaces over K always have a K-rational point when they have dimension at least 8. }, author = {Timothy Browning and Vishe, Pankaj}, journal = {Duke Mathematical Journal}, number = {10}, pages = {1825 -- 1883}, publisher = {Duke University Press}, title = {{Cubic hypersurfaces and a version of the circle method for number fields}}, doi = {10.1215/00127094-2738530}, volume = {163}, year = {2014}, } @article{252, abstract = {For any number field k, upper bounds are established for the number of k-rational points of bounded height on non-singular del Pezzo surfaces defined over k, which are equipped with suitable conic bundle structures over k.}, author = {Timothy Browning and Jones, Michael S}, journal = {Acta Arithmetica}, number = {3}, pages = {271 -- 298}, publisher = {Instytut Matematyczny}, title = {{Counting rational points on del Pezzo surfaces with a conic bundle structure}}, doi = {10.4064/aa163-3-6}, volume = {163}, year = {2014}, } @article{254, abstract = {A new "polynomial sieve" is presented and used to show that almost all integers have at most one representation as a sum of two values of a given polynomial of degree at least 3.}, author = {Timothy Browning}, journal = {International Mathematics Research Notices}, number = {7}, pages = {1987 -- 2019}, publisher = {Oxford University Press}, title = {{The polynomial sieve and equal sums of like polynomials}}, doi = {10.1093/imrn/rnt350}, volume = {2015}, year = {2014}, } @article{255, abstract = {We investigate the Hasse principle for complete intersections cut out by a quadric hypersurface and a cubic hypersurface defined over the rational numbers.}, author = {Browning, Timothy D and Dietmann, Rainer and Heath Brown, Roger}, journal = {Journal of the Institute of Mathematics of Jussieu}, number = {4}, pages = {703 -- 749}, publisher = {Cambridge University Press}, title = {{Rational points on intersections of cubic and quadric hypersurfaces}}, doi = {10.1017/S1474748014000127}, volume = {14}, year = {2014}, } @article{2699, abstract = {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.}, author = {Erdös, László and Bourgade, Paul and Yau, Horng}, journal = {Duke Mathematical Journal}, number = {6}, pages = {1127 -- 1190}, publisher = {Duke University Press}, title = {{Universality of general β-ensembles}}, doi = {10.1215/00127094-2649752}, volume = {163}, year = {2014}, } @article{2716, abstract = {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.}, author = {Chatterjee, Krishnendu and Randour, Mickael and Raskin, Jean}, journal = {Acta Informatica}, number = {3-4}, pages = {129 -- 163}, publisher = {Springer}, title = {{Strategy synthesis for multi-dimensional quantitative objectives}}, doi = {10.1007/s00236-013-0182-6}, volume = {51}, year = {2014}, } @inproceedings{2905, abstract = {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.}, author = {Edelsbrunner, Herbert and Morozovy, Dmitriy}, location = {Kraków, Poland}, pages = {31 -- 50}, publisher = {European Mathematical Society Publishing House}, title = {{Persistent homology: Theory and practice}}, doi = {10.4171/120-1/3}, year = {2014}, } @article{1733, abstract = {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.}, author = {Cerny, Pavol and Chmelik, Martin and Henzinger, Thomas A and Radhakrishna, Arjun}, journal = {Theoretical Computer Science}, number = {3}, pages = {348 -- 363}, publisher = {Elsevier}, title = {{Interface simulation distances}}, doi = {10.1016/j.tcs.2014.08.019}, volume = {560}, year = {2014}, } @article{2141, abstract = {The computation of the winning set for Büchi objectives in alternating games on graphs is a central problem in computer-aided verification with a large number of applications. The long-standing best known upper bound for solving the problem is Õ(n ⋅ m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the Õ(n ⋅ m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2)-time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of Õ(n ⋅ m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m>n4/3 an earlier bound of O(m ⋅ √m)). We then show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. Our algorithms are the first dynamic algorithms for this problem. We then consider another core graph theoretic problem in verification of probabilistic systems, namely computing the maximal end-component decomposition of a graph. We present two improved static algorithms for the maximal end-component decomposition problem. Our first algorithm is an O(m ⋅ √m)-time algorithm, and our second algorithm is an O(n2)-time algorithm which is obtained using the same technique as for alternating Büchi games. Thus, we obtain an O(min &lcu;m ⋅ √m,n2})-time algorithm improving the long-standing O(n ⋅ m) time bound. Finally, we show how to maintain the maximal end-component decomposition of a graph under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per edge deletion, and O(m) worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem.}, author = {Chatterjee, Krishnendu and Henzinger, Monika H}, journal = {Journal of the ACM}, number = {3}, publisher = {ACM}, title = {{Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition}}, doi = {10.1145/2597631}, volume = {61}, year = {2014}, } @article{3263, abstract = {Adaptation in the retina is thought to optimize the encoding of natural light signals into sequences of spikes sent to the brain. While adaptive changes in retinal processing to the variations of the mean luminance level and second-order stimulus statistics have been documented before, no such measurements have been performed when higher-order moments of the light distribution change. We therefore measured the ganglion cell responses in the tiger salamander retina to controlled changes in the second (contrast), third (skew) and fourth (kurtosis) moments of the light intensity distribution of spatially uniform temporally independent stimuli. The skew and kurtosis of the stimuli were chosen to cover the range observed in natural scenes. We quantified adaptation in ganglion cells by studying linear-nonlinear models that capture well the retinal encoding properties across all stimuli. We found that the encoding properties of retinal ganglion cells change only marginally when higher-order statistics change, compared to the changes observed in response to the variation in contrast. By analyzing optimal coding in LN-type models, we showed that neurons can maintain a high information rate without large dynamic adaptation to changes in skew or kurtosis. This is because, for uncorrelated stimuli, spatio-temporal summation within the receptive field averages away non-gaussian aspects of the light intensity distribution.}, author = {Tkacik, Gasper and Ghosh, Anandamohan and Schneidman, Elad and Segev, Ronen}, journal = {PLoS One}, number = {1}, publisher = {Public Library of Science}, title = {{Adaptation to changes in higher-order stimulus statistics in the salamander retina}}, doi = {10.1371/journal.pone.0085841}, volume = {9}, year = {2014}, } @article{332, abstract = {Cu2ZnSnS4, based on abundant and environmental friendly elements and with a direct band gap of 1.5 eV, is a main candidate material for solar energy conversion through both photovoltaics and photocatalysis. We detail here the synthesis of quasi-spherical Cu 2ZnSnS4 nanoparticles with unprecedented narrow size distributions. We further detail their use as seeds to produce CZTS-Au and CZTS-Pt heterostructured nanoparticles. Such heterostructured nanoparticles are shown to have excellent photocatalytic properties toward degradation of Rhodamine B and hydrogen generation by water splitting. }, author = {Yu, Xuelian and Shavel, Alexey and An, Xiaoqiang and Luo, Zhishan and Ibáñez, Maria and Cabot, Andreu}, journal = {Journal of the American Chemical Society}, number = {26}, pages = {9236 -- 9239}, publisher = {ACS}, title = {{Cu2ZnSnS4-Pt and Cu2ZnSnS4-Au heterostructured nanoparticles for photocatalytic water splitting and pollutant degradation}}, doi = {10.1021/ja502076b}, volume = {136}, year = {2014}, } @inproceedings{2054, abstract = {We study two-player concurrent games on finite-state graphs played for an infinite number of rounds, where in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. The objectives are ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). While the qualitative analysis problem for concurrent parity games with infinite-memory, infinite-precision randomized strategies was studied before, we study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision, or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory, or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in (n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based on a characterization of the winning sets as μ-calculus formulas, however, our μ-calculus formulas are crucially different from the ones for concurrent parity games (without bounded rationality); and our memoryless witness strategy constructions are significantly different from the infinite-memory witness strategy constructions for concurrent parity games.}, author = {Chatterjee, Krishnendu}, booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, editor = {Baldan, Paolo and Gorla, Daniele}, location = {Rome, Italy}, pages = {544 -- 559}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Qualitative concurrent parity games: Bounded rationality}}, doi = {10.1007/978-3-662-44584-6_37}, volume = {8704}, year = {2014}, } @article{349, abstract = {Thermoelectricity is a key technology with the potential to improve the efficiency of energy conversion processes, which may strongly benefit from advances in the field of nanotechnology. Nanostructured materials are very appealing for thermoelectric applications, but the full development of their potential requires precise control of their properties at the nanoscale. Bottom-up assembly of nanoparticles provides access to a three-dimensional composition control at the nanoscale not attainable in any other technology. In particular, colloidal nanoheterostructures are especially interesting building blocks for the bottom-up production of functional nanomaterials. In the present work, we use PbTe@PbS core-shell nanoparticles as building blocks for the bottom-up production of PbTe-PbS nanocomposites. We used a ligand exchange strategy and a hot press process to promote the electrical conductivity of the nanocomposite and to increase its density. These two approaches allowed us to improve the performance of bottom-up assembled PbTe-PbS bulk nanostructured materials. }, author = {Ortega, Silvia and Ibáñez, Maria and Cadavid, Doris and Cabot, Andreu}, journal = {International Journal of Nanotechnology}, number = {9-11}, pages = {955 -- 970}, publisher = {Inderscience Enterprises Limited }, title = {{Bottom up processing of PbTe PbS thermoelectric nanocomposites}}, doi = {10.1504/IJNT.2014.063802}, volume = {11}, year = {2014}, } @article{355, abstract = {We report on the photocatalytic hydrogen evolution under full-arc light irradiation of CuIn1-xGaxS2 wurtzite nanocrystals in the presence of SO3 2- and S2- as sacrificial reagents. We analyzed the hydrogen generation rate as a function of the Ga content and associated it with the energy band positions. For photocatalytic water splitting, the CuInS2 bandgap is slightly too low to efficiently overcome the reaction over-potential. The presence of Ga shifts up the CuInS2 conduction band edge providing a larger driving force for photogenerated carriers to activate the water splitting reduction reaction. The larger the Ga content, the more energetically favorable the electron injection, and thus a more efficient use of the photogenerated carriers is reached. However, the band gap increase associated with the Ga incorporation reduces the concentration of photogenerated carriers available for water splitting, and consequently a lower hydrogen conversion rate is obtained for very high Ga contents. The optimum Ga concentration was experimentally found at CuIn0.3Ga0.7S2. }, author = {Yu, Xuelian and An, Xiaoqiang and Shavel, Alexey and Ibáñez, Maria and Cabot, Andreu}, journal = {Journal of Materials Chemistry A}, number = {31}, pages = {12317 -- 12322}, publisher = {Royal Society of Chemistry}, title = {{The effect of the Ga content on the photocatalytic hydrogen evolution of CuIn1-xGaxS2 nanocrystals}}, doi = {10.1039/c4ta01315h}, volume = {2}, year = {2014}, } @article{357, abstract = {Near-resonant Raman scattering measurements of zinc sulfide nanoparticles and thin films have been made and correlated to grain and particle size, respectively, using a 325 nm wavelength excitation source. The area ratios between the first, second, and third order peaks of ZnS identified as the T 2(LO) mode decrease with increasing ZnS grain size. This is an effect attributed to changes in the bandgap energy from quantum confinement due to the varying grain size between the films/particles, as noted by a shift in the room temperature photoluminescence emission corresponding to the free exciton emission energy. While Raman scattering spectroscopy is typically limited to identification of phases and their crystalline properties, it is possible to attain more than such straightforward information by calibrating the spectral features to variations between sets of samples. These results open the possibility of making a quantitative grain size estimation in ZnS thin films and nanostructures, as well as in other material systems where ZnS may be expected as a secondary phase, such as Cu2ZnSnS4. Additionally, more commonly used excitation wavelengths for Raman scattering, such as 514 and 532 nm, are shown to be of limited use in characterizing ZnS thin films due to the extremely low Raman scattering efficiency of ZnS in films with sub-micron thicknesses. }, author = {Fairbrother, Andrew and Izquierdo Roca, Victor and Fontané, Xavier and Ibáñez, Maria and Cabot, Andreu and Saucedo, Edgardo and Pérez Rodríguez, Alejandro}, journal = {CrystEngComm}, number = {20}, pages = {4120 -- 4125}, publisher = {Royal Society of Chemistry}, title = {{ZnS grain size effects on near-resonant Raman scattering: Optical non-destructive grain size estimation}}, doi = {10.1039/c3ce42578a}, volume = {16}, year = {2014}, } @article{359, abstract = {An appropriate way of realizing property nanoengineering in complex quaternary chalcogenide nanocrystals is presented for Cu2Cd xSnSey(CCTSe) polypods. The pivotal role of the polarity in determining morphology, growth, and the polytypic branching mechanism is demonstrated. Polarity is considered to be responsible for the formation of an initial seed that takes the form of a tetrahedron with four cation-polar facets. Size and shape confinement of the intermediate pentatetrahedral seed is also attributed to polarity, as their external facets are anion-polar. The final polypod extensions also branch out as a result of a cation-polarity-driven mechanism. Aberration-corrected scanning transmission electron microscopy is used to identify stannite cation ordering, while ab initio studies are used to show the influence of cation ordering/distortion, stoichiometry, and polytypic structural change on the electronic band structure.}, author = {Zamani, Reza and Ibáñez, Maria and Luysberg, Martina and García Castelló, Nuria and Houben, Lothar and Prades, Joan and Grillo, Vincenzo and Dunin Borkowski, Rafal and Morante, Joan and Cabot, Andreu and Arbiol, Jordi}, journal = {ACS Nano}, number = {3}, pages = {2290 -- 2301}, publisher = {American Chemical Society}, title = {{Polarity-driven polytypic branching in Cu-based quaternary chalcogenide nanostructures}}, doi = {10.1021/nn405747h}, volume = {8}, year = {2014}, } @article{2852, abstract = {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.}, author = {Fischlin, Marc and Lehmann, Anja and Pietrzak, Krzysztof Z}, journal = {Journal of Cryptology}, number = {3}, pages = {397 -- 428}, publisher = {Springer}, title = {{Robust multi-property combiners for hash functions}}, doi = {10.1007/s00145-013-9148-7}, volume = {27}, year = {2014}, } @article{348, abstract = {Bi2S3-xTex bulk nanocomposites with crystal domain sizes in the range from 50 nm to 100 nm were obtained from the reaction of Bi2S3 nanorods with Te powder. The thermoelectric properties of the obtained nanocomposites were analysed in the temperature range from 0°C to 300°C. We observed how the thermoelectric properties of the material improved with the annealing temperature, being a spark plasma sintering process needed to maintain the material nanostructuration while maximising its electrical properties. Finally thermoelectric dimensionless figures of merit ZT up to 0.42 were obtained before any charge carrier concentration optimisation. Copyright © 2014 Inderscience Enterprises Ltd. }, author = {Cadavid, Doris and Ibáñez, Maria and Anselmi Tamburini, Umberto and Durá, Oscar and De La Torre, Marco and Cabot, Andreu}, journal = {International Journal of Nanotechnology}, number = {9-11}, pages = {773 -- 784}, publisher = {Inderscience Enterprises Limited }, title = {{Thermoelectric properties of bottom up assembled Bi2S 3-xTex nanocomposites}}, doi = {10.1504/IJNT.2014.063787}, volume = {11}, year = {2014}, } @article{350, abstract = {Herein, a colloidal synthetic route to produce highly monodisperse Cu2HgGeSe4 (CHGSe) nanoparticles (NPs) is presented in detail. The high yield of the developed procedure allowed the production of CHGSe NPs at the gram scale. A thorough analysis of their structural and optical properties is shown. CHGSe NPs displayed poly-tetrahedral morphology and narrow size distributions with average size in the range of 10–40 nm and size dispersions below 10 %. A 1.6 eV optical band gap was measured by mean of UV–Vis. By adjusting the cation ratio, an effective control of their electrical conductivity is achieved. The prepared NPs are used as building blocks for the production of CHGSe bulk nanostructured materials. The thermoelectric properties of CHGSe nanomaterials are studied in the temperature range from 300 to 730 K. CHGSe nanomaterials reached electrical conductivities up to 5 × 104 S m−1, Seebeck coefficients above 100 μV K−1, and thermal conductivities below 1.0 W m−1 K−1 which translated into thermoelectric figures of merit up to 0.34 at 730 K.}, author = {Li, Wenhua and Ibáñez, Maria and Cadavid, Doris and Zamani, Reza and Rubio Garcia, Javier and Gorsse, Stéphane and Morante, Joan and Arbiol, Jordi and Cabot, Andreu}, journal = {Journal of Nanoparticle Research}, number = {3}, publisher = {Kluwer}, title = {{Colloidal synthesis and functional properties of quaternary Cu based semiconductors: Cu2HgGeSe4}}, doi = {10.1007/s11051-014-2297-2}, volume = {16}, year = {2014}, } @article{356, abstract = {Cu2ZnSnS4, based on abundant and environmental friendly elements and with a direct band gap of 1.5 eV, is a main candidate material for solar energy conversion through both photovoltaics and photocatalysis. We detail here the synthesis of quasi-spherical Cu 2ZnSnS4 nanoparticles with unprecedented narrow size distributions. We further detail their use as seeds to produce CZTS-Au and CZTS-Pt heterostructured nanoparticles. Such heterostructured nanoparticles are shown to have excellent photocatalytic properties toward degradation of Rhodamine B and hydrogen generation by water splitting.}, author = {Yu, Xuelian and Shavel, Alexey and An, Xiaoqiang and Luo, Zhishan and Ibáñez, Maria and Cabot, Andreu}, journal = {Journal of the American Chemical Society}, number = {26}, pages = {9236 -- 9239}, publisher = {American Chemical Society}, title = {{Cu2ZnSnS4-Pt and Cu2ZnSnS4-Au heterostructured nanoparticles for photocatalytic water splitting and pollutant degradation}}, doi = {10.1021/ja502076b}, volume = {136}, year = {2014}, } @article{358, abstract = {Monodispersed Pt3Sn nanoparticles were prepared through a mild thermal synthesis in the presence of surfactants. The performance of Pt3Sn for the electrooxidation of ethanol and adsorbed carbon monoxide (COad) in acid medium was studied by a combination of electrochemical and insitu spectroscopic methods, namely, infrared reflection absorption spectroscopy and differential electrochemical mass spectrometry (DEMS), and the results were compared to those obtained with the use of Pt black. The formation of the Pt3Sn solid solution promoted the oxidation of COad at less-positive potentials than those required for Pt black. Also, the electrooxidation of ethanol, especially at lower potentials, was more favorable with Pt3Sn, as deduced from the higher faradaic currents recorded during the ethanol oxidation reaction (EOR). However, the distribution of products as deduced by DEMS analysis suggested that the formation of C1 products, CO2 inclusive, is less significant on Pt3Sn than on Pt. In fact, the higher faradaic current recorded with the former catalyst can be attributed to the greater amounts of acetaldehyde and acetic acid formed. After the EOR, the surface of both Pt and Pt3Sn remained covered by ethanol adsorbates. Whereas C2 fragments were the main adsorbates at the surface of Pt3Sn after the EOR, both C1 and C2 species remained adsorbed at Pt black.}, author = {Herranz, Tirma and Ibáñez, Maria and Gómez De La Fuente, José and Pérez Alonso, Francisco and Peña, Miguel and Cabot, Andreu and Rojas, Sergio}, journal = {ChemElectroChem}, number = {5}, pages = {885 -- 895}, publisher = {Wiley-Blackwell}, title = {{In situ study of ethanol electrooxidation on monodispersed Pt inf 3 inf Sn nanoparticles}}, doi = {10.1002/celc.201300254}, volume = {1}, year = {2014}, } @article{451, abstract = {We introduce algorithms for the computation of homology, cohomology, and related operations on cubical cell complexes, using the technique based on a chain contraction from the original chain complex to a reduced one that represents its homology. This work is based on previous results for simplicial complexes, and uses Serre’s diagonalization for cubical cells. An implementation in C++ of the introduced algorithms is available at http://www.pawelpilarczyk.com/chaincon/ together with some examples. The paper is self-contained as much as possible, and is written at a very elementary level, so that basic knowledge of algebraic topology should be sufficient to follow it.}, author = {Pawel Pilarczyk and Real, Pedro}, journal = {Advances in Computational Mathematics}, number = {1}, pages = {253 -- 275}, publisher = {Kluwer}, title = {{Computation of cubical homology, cohomology, and (co)homological operations via chain contraction}}, doi = {10.1007/s10444-014-9356-1}, volume = {41}, year = {2014}, } @article{468, abstract = {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.}, author = {Cimadom, Arno and Ulloa, Angel and Meidl, Patrick and Zöttl, Markus and Zöttl, Elisabet and Fessl, Birgit and Nemeth, Erwin and Dvorak, Michael and Cunninghame, Francesca and Tebbich, Sabine}, journal = {PLoS One}, number = {9}, publisher = {Public Library of Science}, title = {{Invasive parasites habitat change and heavy rainfall reduce breeding success in Darwin's finches}}, doi = {10.1371/journal.pone.0107518}, volume = {9}, year = {2014}, } @inproceedings{475, abstract = {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. }, author = {Aminof, Benjamin and Rubin, Sasha}, booktitle = {Electronic Proceedings in Theoretical Computer Science, EPTCS}, location = {Grenoble, France}, pages = {83 -- 90}, publisher = {Open Publishing Association}, title = {{First cycle games}}, doi = {10.4204/EPTCS.146.11}, volume = {146}, year = {2014}, } @inproceedings{10892, abstract = {In this paper, we introduce planar matchings on directed pseudo-line arrangements, which yield a planar set of pseudo-line segments such that only matching-partners are adjacent. By translating the planar matching problem into a corresponding stable roommates problem we show that such matchings always exist. Using our new framework, we establish, for the first time, a complete, rigorous definition of weighted straight skeletons, which are based on a so-called wavefront propagation process. We present a generalized and unified approach to treat structural changes in the wavefront that focuses on the restoration of weak planarity by finding planar matchings.}, author = {Biedl, Therese and Huber, Stefan and Palfrader, Peter}, booktitle = {25th International Symposium, ISAAC 2014}, isbn = {9783319130743}, issn = {1611-3349}, location = {Jeonju, Korea}, pages = {117--127}, publisher = {Springer Nature}, title = {{Planar matchings for weighted straight skeletons}}, doi = {10.1007/978-3-319-13075-0_10}, volume = {8889}, year = {2014}, } @article{537, abstract = {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.}, author = {Prizak, Roshan and Ezard, Thomas and Hoyle, Rebecca}, journal = {Ecology and Evolution}, number = {15}, pages = {3139 -- 3145}, publisher = {Wiley-Blackwell}, title = {{Fitness consequences of maternal and grandmaternal effects}}, doi = {10.1002/ece3.1150}, volume = {4}, year = {2014}, } @inproceedings{1903, abstract = {We consider two-player zero-sum partial-observation stochastic games on graphs. Based on the information available to the players these games can be classified as follows: (a) general partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) perfect-observation (both players have complete view of the game). The one-sided partial-observation games subsumes the important special case of one-player partial-observation stochastic games (or partial-observation Markov decision processes (POMDPs)). Based on the randomization available for the strategies, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. We consider all these classes of games with reachability, and parity objectives that can express all ω-regular objectives. The analysis problems are classified into the qualitative analysis that asks for the existence of a strategy that ensures the objective with probability 1; and the quantitative analysis that asks for the existence of a strategy that ensures the objective with probability at least λ (0,1). In this talk we will cover a wide range of results: for perfect-observation games; for POMDPs; for one-sided partial-observation games; and for general partial-observation games.}, author = {Chatterjee, Krishnendu}, location = {Budapest, Hungary}, number = {PART 1}, pages = {1 -- 4}, publisher = {Springer}, title = {{Partial-observation stochastic reachability and parity games}}, doi = {10.1007/978-3-662-44522-8_1}, volume = {8634}, year = {2014}, } @article{2211, abstract = {In two-player finite-state stochastic games of partial observation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distribution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Our main results for pure strategies are as follows: (1) For one-sided games with player 2 having perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algorithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 having perfect observation we show that nonelementarymemory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least nonelementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibit serious flaws in previous results of the literature: we show a nonelementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, journal = {ACM Transactions on Computational Logic (TOCL)}, number = {2}, publisher = {ACM}, title = {{Partial-observation stochastic games: How to win when belief fails}}, doi = {10.1145/2579821}, volume = {15}, year = {2014}, } @article{2038, abstract = {Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable.}, author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger, Thomas A and Kupferman, Orna}, journal = {ACM Transactions on Computational Logic (TOCL)}, number = {4}, publisher = {ACM}, title = {{Temporal specifications with accumulative values}}, doi = {10.1145/2629686}, volume = {15}, year = {2014}, } @inproceedings{2162, abstract = {We study two-player (zero-sum) concurrent mean-payoff games played on a finite-state graph. We focus on the important sub-class of ergodic games where all states are visited infinitely often with probability 1. The algorithmic study of ergodic games was initiated in a seminal work of Hoffman and Karp in 1966, but all basic complexity questions have remained unresolved. Our main results for ergodic games are as follows: We establish (1) an optimal exponential bound 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); (2) the approximation problem lies in FNP; (3) the approximation problem is at least as hard as the decision problem for simple stochastic games (for which NP ∩ coNP is the long-standing best known bound). We present a variant of the strategy-iteration algorithm by Hoffman and Karp; show that both our algorithm and the classical value-iteration algorithm can approximate the value in exponential time; and identify a subclass where the value-iteration algorithm is a FPTAS. We also show that the exact value can be expressed in the existential theory of the reals, and establish square-root sum hardness for a related class of games.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus}, location = {Copenhagen, Denmark}, number = {Part 2}, pages = {122 -- 133}, publisher = {Springer}, title = {{The complexity of ergodic mean payoff games}}, doi = {10.1007/978-3-662-43951-7_11}, volume = {8573}, year = {2014}, } @inproceedings{2213, abstract = {We consider two-player partial-observation stochastic games on finitestate graphs where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are ε-regular conditions specified as parity objectives. The qualitative-analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). These qualitative-analysis problems are known to be undecidable. However in many applications the relevant question is the existence of finite-memory strategies, and the qualitative-analysis problems under finite-memory strategies was recently shown to be decidable in 2EXPTIME.We improve the complexity and show that the qualitative-analysis problems for partial-observation stochastic parity games under finite-memory strategies are EXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis.}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Nain, Sumit and Vardi, Moshe}, location = {Grenoble, France}, pages = {242 -- 257}, publisher = {Springer}, title = {{The complexity of partial-observation stochastic parity games with finite-memory strategies}}, doi = {10.1007/978-3-642-54830-7_16}, volume = {8412}, year = {2014}, } @inproceedings{2212, abstract = {The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2 1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2 1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic). We present an algorithm running in time O(d·n2d·MeanGame) to compute the set of almost-sure winning states from which the objective can be ensured with probability 1, where n is the number of states of the game, d the number of priorities of the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states in 2 1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective). }, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Oualhadj, Youssouf}, location = {Grenoble, France}, pages = {210 -- 225}, publisher = {Springer}, title = {{Perfect-information stochastic mean-payoff parity games}}, doi = {10.1007/978-3-642-54830-7_14}, volume = {8412}, year = {2014}, } @inproceedings{2216, abstract = {The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition. In this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in time stamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than δ away from the parameter, for δ > 0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and analogous decidability results hold for rectangular automata.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Majumdar, Ritankar}, location = {Berlin, Germany}, pages = {303 -- 312}, publisher = {Springer}, title = {{Edit distance for timed automata}}, doi = {10.1145/2562059.2562141}, year = {2014}, } @misc{5411, abstract = {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.}, author = {Daca, Przemyslaw and Henzinger, Thomas A and Krenn, Willibald and Nickovic, Dejan}, issn = {2664-1690}, pages = {20}, publisher = {IST Austria}, title = {{Compositional specifications for IOCO testing}}, doi = {10.15479/AT:IST-2014-148-v2-1}, year = {2014}, } @misc{5413, abstract = {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. }, author = {Chatterjee, Krishnendu and Daca, Przemyslaw and Chmelik, Martin}, issn = {2664-1690}, pages = {33}, publisher = {IST Austria}, title = {{CEGAR for qualitative analysis of probabilistic systems}}, doi = {10.15479/AT:IST-2014-153-v2-2}, year = {2014}, } @misc{5414, abstract = {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. }, author = {Chatterjee, Krishnendu and Daca, Przemyslaw and Chmelik, Martin}, issn = {2664-1690}, pages = {33}, publisher = {IST Austria}, title = {{CEGAR for qualitative analysis of probabilistic systems}}, doi = {10.15479/AT:IST-2014-153-v3-1}, year = {2014}, } @misc{5412, abstract = {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. }, author = {Chatterjee, Krishnendu and Daca, Przemyslaw and Chmelik, Martin}, issn = {2664-1690}, pages = {31}, publisher = {IST Austria}, title = {{CEGAR for qualitative analysis of probabilistic systems}}, doi = {10.15479/AT:IST-2014-153-v1-1}, year = {2014}, } @inproceedings{2163, abstract = {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 in general, 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. From our results we derive new complexity results for partial-observation stochastic games.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, booktitle = {Lecture Notes in Computer Science}, location = {Copenhagen, Denmark}, number = {Part 2}, pages = {110 -- 121}, publisher = {Springer}, title = {{Games with a weak adversary}}, doi = {10.1007/978-3-662-43951-7_10}, volume = {8573}, year = {2014}, } @misc{5419, abstract = {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.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas}, issn = {2664-1690}, pages = {34}, publisher = {IST Austria}, title = {{Improved algorithms for reachability and shortest path on low tree-width graphs}}, doi = {10.15479/AT:IST-2014-187-v1-1}, year = {2014}, } @inproceedings{2217, abstract = {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.}, author = {Henzinger, Thomas A and Otop, Jan}, booktitle = {Proceedings of the 17th international conference on Hybrid systems: computation and control}, location = {Berlin, Germany}, pages = {213 -- 222}, publisher = {Springer}, title = {{Model measuring for hybrid systems}}, doi = {10.1145/2562059.2562130}, year = {2014}, } @misc{5417, abstract = {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.}, author = {Henzinger, Thomas A and Otop, Jan}, issn = {2664-1690}, pages = {14}, publisher = {IST Austria}, title = {{From model checking to model measuring}}, doi = {10.15479/AT:IST-2014-172-v1-1}, year = {2014}, } @misc{5416, abstract = {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.}, author = {Henzinger, Thomas A and Otop, Jan}, issn = {2664-1690}, pages = {22}, publisher = {IST Austria}, title = {{Model measuring for hybrid systems}}, doi = {10.15479/AT:IST-2014-171-v1-1}, year = {2014}, } @misc{5418, abstract = {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.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, issn = {2664-1690}, pages = {18}, publisher = {IST Austria}, title = {{Games with a weak adversary}}, doi = {10.15479/AT:IST-2014-176-v1-1}, year = {2014}, } @misc{5420, abstract = {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).}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus}, issn = {2664-1690}, pages = {49}, publisher = {IST Austria}, title = {{The value 1 problem for concurrent mean-payoff games}}, doi = {10.15479/AT:IST-2014-191-v1-1}, year = {2014}, } @techreport{5422, abstract = {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.}, author = {Porsche, Jana}, publisher = {none}, title = {{Notes from Research Data Alliance Plenary Meeting in Dublin, Ireland}}, year = {2014}, } @misc{5424, abstract = {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.}, author = {Chatterjee, Krishnendu and Chmelik, Martin and Gupta, Raghav and Kanodia, Ayush}, issn = {2664-1690}, pages = {12}, publisher = {IST Austria}, title = {{Qualitative analysis of POMDPs with temporal logic specifications for robotics applications}}, doi = {10.15479/AT:IST-2014-305-v1-1}, year = {2014}, } @misc{5426, abstract = {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.}, author = {Chatterjee, Krishnendu and Chmelik, Martin and Gupta, Raghav and Kanodia, Ayush}, issn = {2664-1690}, pages = {10}, publisher = {IST Austria}, title = {{Qualitative analysis of POMDPs with temporal logic specifications for robotics applications}}, doi = {10.15479/AT:IST-2014-305-v2-1}, year = {2014}, } @misc{5423, abstract = {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. }, author = {Chatterjee, Krishnendu and Kössler, Alexander and Pavlogiannis, Andreas and Schmid, Ulrich}, issn = {2664-1690}, pages = {14}, publisher = {IST Austria}, title = {{A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks}}, doi = {10.15479/AT:IST-2014-300-v1-1}, year = {2014}, } @misc{5427, abstract = {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.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas}, issn = {2664-1690}, pages = {24}, publisher = {IST Austria}, title = {{Optimal tree-decomposition balancing and reachability on low treewidth graphs}}, doi = {10.15479/AT:IST-2014-314-v1-1}, year = {2014}, } @misc{5425, abstract = { 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.}, author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3 and Anonymous, 4}, issn = {2664-1690}, pages = {22}, publisher = {IST Austria}, title = {{Optimal cost almost-sure reachability in POMDPs}}, year = {2014}, } @misc{5415, abstract = {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. }, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, issn = {2664-1690}, pages = {27}, publisher = {IST Austria}, title = {{Nested weighted automata}}, doi = {10.15479/AT:IST-2014-170-v1-1}, year = {2014}, } @misc{5421, abstract = {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.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Nowak, Martin}, issn = {2664-1690}, pages = {27}, publisher = {IST Austria}, title = {{The complexity of evolution on graphs}}, doi = {10.15479/AT:IST-2014-190-v2-2}, year = {2014}, } @article{5813, abstract = {We consider homogeneous Bose gas in a large cubic box with periodic boundary conditions, at zero temperature. We analyze its excitation spectrum in a certain kind of a mean-field infinite-volume limit. We prove that under appropriate conditions the excitation spectrum has the form predicted by the Bogoliubov approximation. Our result can be viewed as an extension of the result of Seiringer (Commun. Math. Phys.306:565–578, 2011) to large volumes.}, author = {Dereziński, Jan and Napiórkowski, Marcin M}, issn = {1424-0637}, journal = {Annales Henri Poincaré}, number = {12}, pages = {2409--2439}, publisher = {Springer Nature}, title = {{Excitation spectrum of interacting bosons in the Mean-Field Infinite-Volume limit}}, doi = {10.1007/s00023-013-0302-4}, volume = {15}, year = {2014}, } @inproceedings{5810, abstract = {A discrete spherical geodesic path between two voxels s and t lying on a discrete sphere is a/the 1-connected shortest path from s to t, comprising voxels of the discrete sphere intersected by the real plane passing through s, t, and the center of the sphere. We show that the set of sphere voxels intersected by the aforesaid real plane always contains a 1-connected cycle passing through s and t, and each voxel in this set lies within an isothetic distance of 32 from the concerned plane. Hence, to compute the path, the algorithm starts from s, and iteratively computes each voxel p of the path from the predecessor of p. A novel number-theoretic property and the 48-symmetry of discrete sphere are used for searching the 1-connected voxels comprising the path. The algorithm is output-sensitive, having its time and space complexities both linear in the length of the path. It can be extended for constructing 1-connected discrete 3D circles of arbitrary orientations, specified by a few appropriate input parameters. Experimental results and related analysis demonstrate its efficiency and versatility.}, author = {Biswas, Ranita and Bhowmick, Partha}, isbn = {9783642387081}, issn = {0302-9743}, location = {Siena, Italy}, pages = {396--409}, publisher = {Springer}, title = {{On Finding Spherical Geodesic Paths and Circles in ℤ3}}, doi = {10.1007/978-3-319-09955-2_33}, volume = {8668}, year = {2014}, }