@inproceedings{1603, abstract = {For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation. The key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Chmelik, Martin and Fellner, Andreas and Kretinsky, Jan}, location = {San Francisco, CA, United States}, pages = {158 -- 177}, publisher = {Springer}, title = {{Counterexample explanation by learning small strategies in Markov decision processes}}, doi = {10.1007/978-3-319-21690-4_10}, volume = {9206}, year = {2015}, } @misc{5549, abstract = {This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. We extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees. The archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library. To execute the program, please have a look at the README.txt, which provides instructions and further information on the archive. The archive contains scripts that (if run often enough) reproduces the data presented in the publication.}, author = {Fellner, Andreas}, keywords = {Markov Decision Process, Decision Tree, Probabilistic Verification, Counterexample Explanation}, publisher = {Institute of Science and Technology Austria}, title = {{Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes}}, doi = {10.15479/AT:ISTA:28}, year = {2015}, } @inproceedings{1512, abstract = {We show that very weak topological assumptions are enough to ensure the existence of a Helly-type theorem. More precisely, we show that for any non-negative integers b and d there exists an integer h(b,d) such that the following holds. If F is a finite family of subsets of R^d such that the ith reduced Betti number (with Z_2 coefficients in singular homology) of the intersection of any proper subfamily G of F is at most b for every non-negative integer i less or equal to (d-1)/2, then F has Helly number at most h(b,d). These topological conditions are sharp: not controlling any of these first Betti numbers allow for families with unbounded Helly number. Our proofs combine homological non-embeddability results with a Ramsey-based approach to build, given an arbitrary simplicial complex K, some well-behaved chain map from C_*(K) to C_*(R^d). Both techniques are of independent interest.}, author = {Goaoc, Xavier and Paták, Pavel and Patakova, Zuzana and Tancer, Martin and Wagner, Uli}, location = {Eindhoven, Netherlands}, pages = {507 -- 521}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Bounding Helly numbers via Betti numbers}}, doi = {10.4230/LIPIcs.SOCG.2015.507}, volume = {34}, year = {2015}, } @article{271, abstract = {We show that a non-singular integral form of degree d is soluble non-trivially over the integers if and only if it is soluble non-trivially over the reals and the p-adic numbers, provided that the form has at least (d-\sqrt{d}/2)2^d variables. This improves on a longstanding result of Birch.}, author = {Browning, Timothy D and Prendiville, Sean}, issn = {0075-4102}, journal = {Journal fur die Reine und Angewandte Mathematik}, number = {731}, pages = {203 -- 234}, publisher = {Walter de Gruyter}, title = {{Improvements in Birch's theorem on forms in many variables}}, doi = {10.1515/crelle-2014-0122}, volume = {2017}, year = {2015}, } @inproceedings{1675, abstract = {Proofs of work (PoW) have been suggested by Dwork and Naor (Crypto’92) as protection to a shared resource. The basic idea is to ask the service requestor to dedicate some non-trivial amount of computational work to every request. The original applications included prevention of spam and protection against denial of service attacks. More recently, PoWs have been used to prevent double spending in the Bitcoin digital currency system. In this work, we put forward an alternative concept for PoWs - so-called proofs of space (PoS), where a service requestor must dedicate a significant amount of disk space as opposed to computation. We construct secure PoS schemes in the random oracle model (with one additional mild assumption required for the proof to go through), using graphs with high “pebbling complexity” and Merkle hash-trees. We discuss some applications, including follow-up work where a decentralized digital currency scheme called Spacecoin is constructed that uses PoS (instead of wasteful PoW like in Bitcoin) to prevent double spending. The main technical contribution of this work is the construction of (directed, loop-free) graphs on N vertices with in-degree O(log logN) such that even if one places Θ(N) pebbles on the nodes of the graph, there’s a constant fraction of nodes that needs Θ(N) steps to be pebbled (where in every step one can put a pebble on a node if all its parents have a pebble).}, author = {Dziembowski, Stefan and Faust, Sebastian and Kolmogorov, Vladimir and Pietrzak, Krzysztof Z}, booktitle = {35th Annual Cryptology Conference}, isbn = {9783662479995}, issn = {0302-9743}, location = {Santa Barbara, CA, United States}, pages = {585 -- 605}, publisher = {Springer}, title = {{Proofs of space}}, doi = {10.1007/978-3-662-48000-7_29}, volume = {9216}, year = {2015}, } @article{15160, abstract = {The circadian clock orchestrates global changes in transcriptional regulation on a daily basis via the bHLH-PAS transcription factor CLOCK:BMAL1. Pathways driven by other bHLH-PAS transcription factors have a homologous repressor that modulates activity on a tissue-specific basis, but none have been identified for CLOCK:BMAL1. We show here that the cancer/testis antigen PASD1 fulfills this role to suppress circadian rhythms. PASD1 is evolutionarily related to CLOCK and interacts with the CLOCK:BMAL1 complex to repress transcriptional activation. Expression of PASD1 is restricted to germline tissues in healthy individuals but can be induced in cells of somatic origin upon oncogenic transformation. Reducing PASD1 in human cancer cells significantly increases the amplitude of transcriptional oscillations to generate more robust circadian rhythms. Our results describe a function for a germline-specific protein in regulation of the circadian clock and provide a molecular link from oncogenic transformation to suppression of circadian rhythms.}, author = {Michael, Alicia Kathleen and Harvey, Stacy L. and Sammons, Patrick J. and Anderson, Amanda P. and Kopalle, Hema M. and Banham, Alison H. and Partch, Carrie L.}, issn = {1097-2765}, journal = {Molecular Cell}, keywords = {Cell Biology, Molecular Biology}, number = {5}, pages = {743--754}, publisher = {Elsevier}, title = {{Cancer/Testis antigen PASD1 silences the circadian clock}}, doi = {10.1016/j.molcel.2015.03.031}, volume = {58}, year = {2015}, } @article{15159, abstract = {It is widely recognized that BMAL1 is an essential subunit of the primary transcription factor that drives rhythmic circadian transcription in the nucleus. In a surprising turn, Lipton et al. now show that BMAL1 rhythmically interacts with translational machinery in the cytosol to stimulate protein synthesis in response to mTOR signaling.}, author = {Michael, Alicia Kathleen and Asimgil, Hande and Partch, Carrie L.}, issn = {0968-0004}, journal = {Trends in Biochemical Sciences}, keywords = {Molecular Biology, Biochemistry}, number = {9}, pages = {489--490}, publisher = {Elsevier}, title = {{Cytosolic BMAL1 moonlights as a translation factor}}, doi = {10.1016/j.tibs.2015.07.006}, volume = {40}, year = {2015}, } @article{1619, abstract = {The emergence of drug resistant pathogens is a serious public health problem. It is a long-standing goal to predict rates of resistance evolution and design optimal treatment strategies accordingly. To this end, it is crucial to reveal the underlying causes of drug-specific differences in the evolutionary dynamics leading to resistance. However, it remains largely unknown why the rates of resistance evolution via spontaneous mutations and the diversity of mutational paths vary substantially between drugs. Here we comprehensively quantify the distribution of fitness effects (DFE) of mutations, a key determinant of evolutionary dynamics, in the presence of eight antibiotics representing the main modes of action. Using precise high-throughput fitness measurements for genome-wide Escherichia coli gene deletion strains, we find that the width of the DFE varies dramatically between antibiotics and, contrary to conventional wisdom, for some drugs the DFE width is lower than in the absence of stress. We show that this previously underappreciated divergence in DFE width among antibiotics is largely caused by their distinct drug-specific dose-response characteristics. Unlike the DFE, the magnitude of the changes in tolerated drug concentration resulting from genome-wide mutations is similar for most drugs but exceptionally small for the antibiotic nitrofurantoin, i.e., mutations generally have considerably smaller resistance effects for nitrofurantoin than for other drugs. A population genetics model predicts that resistance evolution for drugs with this property is severely limited and confined to reproducible mutational paths. We tested this prediction in laboratory evolution experiments using the “morbidostat”, a device for evolving bacteria in well-controlled drug environments. Nitrofurantoin resistance indeed evolved extremely slowly via reproducible mutations—an almost paradoxical behavior since this drug causes DNA damage and increases the mutation rate. Overall, we identified novel quantitative characteristics of the evolutionary landscape that provide the conceptual foundation for predicting the dynamics of drug resistance evolution.}, author = {Chevereau, Guillaume and Dravecka, Marta and Batur, Tugce and Guvenek, Aysegul and Ayhan, Dilay and Toprak, Erdal and Bollenbach, Mark Tobias}, journal = {PLoS Biology}, number = {11}, publisher = {Public Library of Science}, title = {{Quantifying the determinants of evolutionary dynamics leading to drug resistance}}, doi = {10.1371/journal.pbio.1002299}, volume = {13}, year = {2015}, } @article{10382, abstract = {Protein oligomers have been implicated as toxic agents in a wide range of amyloid-related diseases. However, it has remained unsolved whether the oligomers are a necessary step in the formation of amyloid fibrils or just a dangerous byproduct. Analogously, it has not been resolved if the amyloid nucleation process is a classical one-step nucleation process or a two-step process involving prenucleation clusters. We use coarse-grained computer simulations to study the effect of nonspecific attractions between peptides on the primary nucleation process underlying amyloid fibrillization. We find that, for peptides that do not attract, the classical one-step nucleation mechanism is possible but only at nonphysiologically high peptide concentrations. At low peptide concentrations, which mimic the physiologically relevant regime, attractive interpeptide interactions are essential for fibril formation. Nucleation then inevitably takes place through a two-step mechanism involving prefibrillar oligomers. We show that oligomers not only help peptides meet each other but also, create an environment that facilitates the conversion of monomers into the β-sheet–rich form characteristic of fibrils. Nucleation typically does not proceed through the most prevalent oligomers but through an oligomer size that is only observed in rare fluctuations, which is why such aggregates might be hard to capture experimentally. Finally, we find that the nucleation of amyloid fibrils cannot be described by classical nucleation theory: in the two-step mechanism, the critical nucleus size increases with increases in both concentration and interpeptide interactions, which is in direct contrast with predictions from classical nucleation theory.}, author = {Šarić, Anđela and Chebaro, Yassmine C. and Knowles, Tuomas P. J. and Frenkel, Daan}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, keywords = {multidisciplinary}, number = {50}, pages = {17869--17874}, publisher = {National Academy of Sciences}, title = {{Crucial role of nonspecific interactions in amyloid nucleation}}, doi = {10.1073/pnas.1410159111}, volume = {111}, year = {2014}, } @article{10383, abstract = {We use numerical simulations to compute the equation of state of a suspension of spherical self-propelled nanoparticles in two and three dimensions. We study in detail the effect of excluded volume interactions and confinement as a function of the system's temperature, concentration, and strength of the propulsion. We find a striking nonmonotonic dependence of the pressure on the temperature and provide simple scaling arguments to predict and explain the occurrence of such anomalous behavior. We explicitly show how our results have important implications for the effective forces on passive components suspended in a bath of active particles.}, author = {Mallory, S. A. and Šarić, Anđela and Valeriani, C. and Cacciuto, A.}, issn = {1550-2376}, journal = {Physical Review E}, number = {5}, publisher = {American Physical Society}, title = {{Anomalous thermomechanical properties of a self-propelled colloidal fluid}}, doi = {10.1103/physreve.89.052303}, volume = {89}, year = {2014}, }