@inproceedings{1690, abstract = {A number of powerful and scalable hybrid systems model checkers have recently emerged. Although all of them honor roughly the same hybrid systems semantics, they have drastically different model description languages. This situation (a) makes it difficult to quickly evaluate a specific hybrid automaton model using the different tools, (b) obstructs comparisons of reachability approaches, and (c) impedes the widespread application of research results that perform model modification and could benefit many of the tools. In this paper, we present Hyst, a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation passes that serve to both ease the translation and potentially improve reachability results for the supported tools. Although these model transformation passes could be implemented within each tool, the Hyst approach provides a single place for model modification, generating modified input sources for the unmodified target tools. Our evaluation demonstrates Hyst is capable of automatically translating benchmarks in several classes (including affine and nonlinear hybrid automata) to the input formats of several tools. Additionally, we illustrate a general model transformation pass based on pseudo-invariants implemented in Hyst that illustrates the reachability improvement.}, author = {Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor}, location = {Seattle, WA, United States}, pages = {128 -- 133}, publisher = {Springer}, title = {{HYST: A source transformation and translation tool for hybrid automaton models}}, doi = {10.1145/2728606.2728630}, year = {2015}, } @inproceedings{1691, abstract = {We consider a case study of the problem of deploying an autonomous air vehicle in a partially observable, dynamic, indoor environment from a specification given as a linear temporal logic (LTL) formula over regions of interest. We model the motion and sensing capabilities of the vehicle as a partially observable Markov decision process (POMDP). We adapt recent results for solving POMDPs with parity objectives to generate a control policy. We also extend the existing framework with a policy minimization technique to obtain a better implementable policy, while preserving its correctness. The proposed techniques are illustrated in an experimental setup involving an autonomous quadrotor performing surveillance in a dynamic environment.}, author = {Svoreňová, Mária and Chmelik, Martin and Leahy, Kevin and Eniser, Hasan and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, location = {Seattle, WA, United States}, pages = {233 -- 238}, publisher = {ACM}, title = {{Temporal logic motion planning using POMDPs with parity objectives: Case study paper}}, doi = {10.1145/2728606.2728617}, year = {2015}, } @article{1694, abstract = { We introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata. }, author = {Chatterjee, Krishnendu and Prabhu, Vinayak}, journal = {IEEE Transactions on Automatic Control}, number = {9}, pages = {2291 -- 2306}, publisher = {IEEE}, title = {{Quantitative temporal simulation and refinement distances for timed systems}}, doi = {10.1109/TAC.2015.2404612}, volume = {60}, year = {2015}, } @article{1695, abstract = {We give a comprehensive introduction into a diagrammatic method that allows for the evaluation of Gutzwiller wave functions in finite spatial dimensions. We discuss in detail some numerical schemes that turned out to be useful in the real-space evaluation of the diagrams. The method is applied to the problem of d-wave superconductivity in a two-dimensional single-band Hubbard model. Here, we discuss in particular the role of long-range contributions in our diagrammatic expansion. We further reconsider our previous analysis on the kinetic energy gain in the superconducting state.}, author = {Kaczmarczyk, Jan and Schickling, Tobias and Bünemann, Jörg}, journal = {Physica Status Solidi (B): Basic Solid State Physics}, number = {9}, pages = {2059 -- 2071}, publisher = {Wiley}, title = {{Evaluation techniques for Gutzwiller wave functions in finite dimensions}}, doi = {10.1002/pssb.201552082}, volume = {252}, year = {2015}, } @article{1697, abstract = {Motion tracking is a challenge the visual system has to solve by reading out the retinal population. It is still unclear how the information from different neurons can be combined together to estimate the position of an object. Here we recorded a large population of ganglion cells in a dense patch of salamander and guinea pig retinas while displaying a bar moving diffusively. We show that the bar’s position can be reconstructed from retinal activity with a precision in the hyperacuity regime using a linear decoder acting on 100+ cells. We then took advantage of this unprecedented precision to explore the spatial structure of the retina’s population code. The classical view would have suggested that the firing rates of the cells form a moving hill of activity tracking the bar’s position. Instead, we found that most ganglion cells in the salamander fired sparsely and idiosyncratically, so that their neural image did not track the bar. Furthermore, ganglion cell activity spanned an area much larger than predicted by their receptive fields, with cells coding for motion far in their surround. As a result, population redundancy was high, and we could find multiple, disjoint subsets of neurons that encoded the trajectory with high precision. This organization allows for diverse collections of ganglion cells to represent high-accuracy motion information in a form easily read out by downstream neural circuits.}, author = {Marre, Olivier and Botella Soler, Vicente and Simmons, Kristina and Mora, Thierry and Tkacik, Gasper and Berry, Michael}, journal = {PLoS Computational Biology}, number = {7}, publisher = {Public Library of Science}, title = {{High accuracy decoding of dynamical motion from a large retinal population}}, doi = {10.1371/journal.pcbi.1004304}, volume = {11}, year = {2015}, } @article{1699, abstract = {By hybridization and backcrossing, alleles can surmount species boundaries and be incorporated into the genome of a related species. This introgression of genes is of particular evolutionary relevance if it involves the transfer of adaptations between populations. However, any beneficial allele will typically be associated with other alien alleles that are often deleterious and hamper the introgression process. In order to describe the introgression of an adaptive allele, we set up a stochastic model with an explicit genetic makeup of linked and unlinked deleterious alleles. Based on the theory of reducible multitype branching processes, we derive a recursive expression for the establishment probability of the beneficial allele after a single hybridization event. We furthermore study the probability that slightly deleterious alleles hitchhike to fixation. The key to the analysis is a split of the process into a stochastic phase in which the advantageous alleles establishes and a deterministic phase in which it sweeps to fixation. We thereafter apply the theory to a set of biologically relevant scenarios such as introgression in the presence of many unlinked or few closely linked deleterious alleles. A comparison to computer simulations shows that the approximations work well over a large parameter range.}, author = {Uecker, Hildegard and Setter, Derek and Hermisson, Joachim}, journal = {Journal of Mathematical Biology}, number = {7}, pages = {1523 -- 1580}, publisher = {Springer}, title = {{Adaptive gene introgression after secondary contact}}, doi = {10.1007/s00285-014-0802-y}, volume = {70}, year = {2015}, } @article{1696, abstract = {The recently proposed diagrammatic expansion (DE) technique for the full Gutzwiller wave function (GWF) is applied to the Anderson lattice model. This approach allows for a systematic evaluation of the expectation values with full Gutzwiller wave function in finite-dimensional systems. It introduces results extending in an essential manner those obtained by means of the standard Gutzwiller approximation (GA), which is variationally exact only in infinite dimensions. Within the DE-GWF approach we discuss the principal paramagnetic properties and their relevance to heavy-fermion systems. We demonstrate the formation of an effective, narrow f band originating from atomic f-electron states and subsequently interpret this behavior as a direct itineracy of f electrons; it represents a combined effect of both the hybridization and the correlations induced by the Coulomb repulsive interaction. Such a feature is absent on the level of GA, which is equivalent to the zeroth order of our expansion. Formation of the hybridization- and electron-concentration-dependent narrow f band rationalizes the common assumption of such dispersion of f levels in the phenomenological modeling of the band structure of CeCoIn5. Moreover, it is shown that the emerging f-electron direct itineracy leads in a natural manner to three physically distinct regimes within a single model that are frequently discussed for 4f- or 5f-electron compounds as separate model situations. We identify these regimes as (i) the mixed-valence regime, (ii) Kondo/almost-Kondo insulating regime, and (iii) the Kondo-lattice limit when the f-electron occupancy is very close to the f-state half filling, ⟨nˆf⟩→1. The nonstandard features of the emerging correlated quantum liquid state are stressed.}, author = {Wysokiński, Marcin and Kaczmarczyk, Jan and Spałek, Jozef}, journal = {Physical Review B}, number = {12}, publisher = {American Physical Society}, title = {{Gutzwiller wave function solution for Anderson lattice model: Emerging universal regimes of heavy quasiparticle states}}, doi = {10.1103/PhysRevB.92.125135}, volume = {92}, year = {2015}, } @article{1701, abstract = {The activity of a neural network is defined by patterns of spiking and silence from the individual neurons. Because spikes are (relatively) sparse, patterns of activity with increasing numbers of spikes are less probable, but, with more spikes, the number of possible patterns increases. This tradeoff between probability and numerosity is mathematically equivalent to the relationship between entropy and energy in statistical physics. We construct this relationship for populations of up to N = 160 neurons in a small patch of the vertebrate retina, using a combination of direct and model-based analyses of experiments on the response of this network to naturalistic movies. We see signs of a thermodynamic limit, where the entropy per neuron approaches a smooth function of the energy per neuron as N increases. The form of this function corresponds to the distribution of activity being poised near an unusual kind of critical point. We suggest further tests of criticality, and give a brief discussion of its functional significance. }, author = {Tkacik, Gasper and Mora, Thierry and Marre, Olivier and Amodei, Dario and Palmer, Stephanie and Berry Ii, Michael and Bialek, William}, journal = {PNAS}, number = {37}, pages = {11508 -- 11513}, publisher = {National Academy of Sciences}, title = {{Thermodynamics and signatures of criticality in a network of neurons}}, doi = {10.1073/pnas.1514188112}, volume = {112}, year = {2015}, } @article{1698, abstract = {In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete.}, author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A and Rabinovich, Alexander and Raskin, Jean}, journal = {Information and Computation}, number = {4}, pages = {177 -- 196}, publisher = {Elsevier}, title = {{The complexity of multi-mean-payoff and multi-energy games}}, doi = {10.1016/j.ic.2015.03.001}, volume = {241}, year = {2015}, } @article{1700, abstract = {We use the dual boson approach to reveal the phase diagram of the Fermi-Hubbard model with long-range dipole-dipole interactions. By using a large-scale finite-temperature calculation on a 64×64 square lattice we demonstrate the existence of a novel phase, possessing an "ultralong-range" order. The fingerprint of this phase - the density correlation function - features a nontrivial behavior on a scale of tens of lattice sites. We study the properties and the stability of the ultralong-range-ordered phase, and show that it is accessible in modern experiments with ultracold polar molecules and magnetic atoms.}, author = {Van Loon, Erik and Katsnelson, Mikhail and Lemeshko, Mikhail}, journal = {Physical Review B}, number = {8}, publisher = {American Physical Society}, title = {{Ultralong-range order in the Fermi-Hubbard model with long-range interactions}}, doi = {10.1103/PhysRevB.92.081106}, volume = {92}, year = {2015}, }