@inproceedings{2847,
abstract = {Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.},
author = {Bansal, Kshitij and Koskinen, Eric and Wies, Thomas and Zufferey, Damien},
editor = {Piterman, Nir and Smolka, Scott},
location = {Rome, Italy},
pages = {62 -- 77},
publisher = {Springer},
title = {{Structural Counter Abstraction}},
doi = {10.1007/978-3-642-36742-7_5},
volume = {7795},
year = {2013},
}
@inproceedings{2445,
abstract = {We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten},
location = {St. Petersburg, Russia},
pages = {951 -- 967},
publisher = {Springer},
title = {{Efficient synthesis for concurrency by semantics-preserving transformations}},
doi = {10.1007/978-3-642-39799-8_68},
volume = {8044},
year = {2013},
}
@article{2263,
abstract = {Nestin-cre transgenic mice have been widely used to direct recombination to neural stem cells (NSCs) and intermediate neural progenitor cells (NPCs). Here we report that a readily utilized, and the only commercially available, Nestin-cre line is insufficient for directing recombination in early embryonic NSCs and NPCs. Analysis of recombination efficiency in multiple cre-dependent reporters and a genetic mosaic line revealed consistent temporal and spatial patterns of recombination in NSCs and NPCs. For comparison we utilized a knock-in Emx1cre line and found robust recombination in NSCs and NPCs in ventricular and subventricular zones of the cerebral cortices as early as embryonic day 12.5. In addition we found that the rate of Nestin-cre driven recombination only reaches sufficiently high levels in NSCs and NPCs during late embryonic and early postnatal periods. These findings are important when commercially available cre lines are considered for directing recombination to embryonic NSCs and NPCs.},
author = {Liang, Huixuan and Hippenmeyer, Simon and Ghashghaei, H.},
journal = {Biology open},
number = {12},
pages = {1200 -- 1203},
publisher = {The Company of Biologists},
title = {{A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors}},
doi = {10.1242/bio.20122287},
volume = {1},
year = {2012},
}
@article{2302,
abstract = {We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only "significant" mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model's variables.},
author = {Henzinger, Thomas A and Mateescu, Maria},
journal = {IEEE ACM Transactions on Computational Biology and Bioinformatics},
number = {2},
pages = {310 -- 322},
publisher = {IEEE},
title = {{The propagation approach for computing biochemical reaction networks}},
doi = {10.1109/TCBB.2012.91},
volume = {10},
year = {2012},
}
@article{2318,
abstract = {We show that bosons interacting via pair potentials with negative scattering length form bound states for a suitable number of particles. In other words, the absence of many-particle bound states of any kind implies the non-negativity of the scattering length of the interaction potential. },
author = {Seiringer, Robert},
journal = {Journal of Spectral Theory},
number = {3},
pages = {321--328},
publisher = {European Mathematical Society},
title = {{Absence of bound states implies non-negativity of the scattering length}},
doi = {10.4171/JST/31},
volume = {2},
year = {2012},
}
@article{2411,
abstract = {The kingdom of fungi provides model organisms for biotechnology, cell biology, genetics, and life sciences in general. Only when their phylogenetic relationships are stably resolved, can individual results from fungal research be integrated into a holistic picture of biology. However, and despite recent progress, many deep relationships within the fungi remain unclear. Here, we present the first phylogenomic study of an entire eukaryotic kingdom that uses a consistency criterion to strengthen phylogenetic conclusions. We reason that branches (splits) recovered with independent data and different tree reconstruction methods are likely to reflect true evolutionary relationships. Two complementary phylogenomic data sets based on 99 fungal genomes and 109 fungal expressed sequence tag (EST) sets analyzed with four different tree reconstruction methods shed light from different angles on the fungal tree of life. Eleven additional data sets address specifically the phylogenetic position of Blastocladiomycota, Ustilaginomycotina, and Dothideomycetes, respectively. The combined evidence from the resulting trees supports the deep-level stability of the fungal groups toward a comprehensive natural system of the fungi. In addition, our analysis reveals methodologically interesting aspects. Enrichment for EST encoded data-a common practice in phylogenomic analyses-introduces a strong bias toward slowly evolving and functionally correlated genes. Consequently, the generalization of phylogenomic data sets as collections of randomly selected genes cannot be taken for granted. A thorough characterization of the data to assess possible influences on the tree reconstruction should therefore become a standard in phylogenomic analyses.},
author = {Ebersberger, Ingo and De Matos Simoes, Ricardo and Kupczok, Anne and Gube, Matthias and Kothe, Erika and Voigt, Kerstin and Von Haeseler, Arndt},
journal = {Molecular Biology and Evolution},
number = {5},
pages = {1319 -- 1334},
publisher = {Oxford University Press},
title = {{A consistent phylogenetic backbone for the fungi}},
doi = {10.1093/molbev/msr285},
volume = {29},
year = {2012},
}
@inproceedings{2715,
abstract = {We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning vertices from where the objective can be ensured with probability 1. We study for the first time the average case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average case running time is linear (as compared to the worst case linear number of iterations and quadratic time complexity). Second, for the average case analysis over all MDPs we show that the expected number of iterations is constant and the average case running time is linear (again as compared to the worst case linear number of iterations and quadratic time complexity). Finally we also show that given that all MDPs are equally likely, the probability that the classical algorithm requires more than constant number of iterations is exponentially small.},
author = {Chatterjee, Krishnendu and Joglekar, Manas and Shah, Nisarg},
location = {Hyderabad, India},
pages = {461 -- 473},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives}},
doi = {10.4230/LIPIcs.FSTTCS.2012.461},
volume = {18},
year = {2012},
}
@inproceedings{2825,
abstract = {We study the problem of maximum marginal prediction (MMP) in probabilistic graphical models, a task that occurs, for example, as the Bayes optimal decision rule under a Hamming loss. MMP is typically performed as a two-stage procedure: one estimates each variable's marginal probability and then forms a prediction from the states of maximal probability. In this work we propose a simple yet effective technique for accelerating MMP when inference is sampling-based: instead of the above two-stage procedure we directly estimate the posterior probability of each decision variable. This allows us to identify the point of time when we are sufficiently certain about any individual decision. Whenever this is the case, we dynamically prune the variables we are confident about from the underlying factor graph. Consequently, at any time only samples of variables whose decision is still uncertain need to be created. Experiments in two prototypical scenarios, multi-label classification and image inpainting, show that adaptive sampling can drastically accelerate MMP without sacrificing prediction accuracy.},
author = {Lampert, Christoph},
location = {Lake Tahoe, NV, United States},
pages = {82 -- 90},
publisher = {Neural Information Processing Systems},
title = {{Dynamic pruning of factor graphs for maximum marginal prediction}},
volume = {1},
year = {2012},
}
@article{2848,
abstract = {We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics.},
author = {Chatterjee, Krishnendu and Zufferey, Damien and Nowak, Martin},
journal = {Journal of Theoretical Biology},
pages = {161 -- 173},
publisher = {Elsevier},
title = {{Evolutionary game dynamics in populations with different learners}},
doi = {10.1016/j.jtbi.2012.02.021},
volume = {301},
year = {2012},
}
@article{2849,
author = {Edelsbrunner, Herbert and Strelkova, Nataliya},
journal = {Russian Mathematical Surveys},
number = {6},
pages = {1167 -- 1168},
publisher = {IOP Publishing Ltd.},
title = {{On the configuration space of Steiner minimal trees}},
doi = {10.1070/RM2012v067n06ABEH004820},
volume = {67},
year = {2012},
}