@inproceedings{1205,
abstract = {In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.},
author = {Jiang, Yu and Liu, Han and Song, Houbing and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui},
location = {Limassol, Cyprus},
pages = {757 -- 763},
publisher = {Springer},
title = {{Safety assured formal model driven design of the multifunction vehicle bus controller}},
doi = {10.1007/978-3-319-48989-6_47},
volume = {9995},
year = {2016},
}
@inproceedings{478,
abstract = {Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus},
location = {The Hague, Netherlands},
pages = {1432 -- 1439},
publisher = {IOS Press},
title = {{The complexity of deciding legality of a single step of magic: The gathering}},
doi = {10.3233/978-1-61499-672-9-1432},
volume = {285},
year = {2016},
}
@inproceedings{480,
abstract = {Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for -approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements.},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
location = {New York, NY, USA},
pages = {247 -- 256},
publisher = {IEEE},
title = {{Perfect-information stochastic games with generalized mean-payoff objectives}},
doi = {10.1145/2933575.2934513},
volume = {05-08-July-2016},
year = {2016},
}
@inproceedings{1234,
abstract = {We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.},
author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana},
location = {Eindhoven, The Netherlands},
pages = {112 -- 129},
publisher = {Springer},
title = {{Faster statistical model checking for unbounded temporal properties}},
doi = {10.1007/978-3-662-49674-9_7},
volume = {9636},
year = {2016},
}
@article{510,
abstract = {The CLE (CLAVATA3/Embryo Surrounding Region-related) peptides are small secreted signaling peptides that are primarily involved in the regulation of stem cell homeostasis in different plant meristems. Particularly, the characterization of the CLE41-PXY/TDR signaling pathway has greatly advanced our understanding on the potential roles of CLE peptides in vascular development and wood formation. Nevertheless, our knowledge on this gene family in a tree species is limited. In a recent study, we reported on a systematically investigation of the CLE gene family in Populus trichocarpa . The potential roles of PtCLE genes were studied by comparative analysis and transcriptional pro fi ling. Among fi fty PtCLE members, many PtCLE proteins share identical CLE motifs or contain the same CLE motif as that of AtCLEs, while PtCLE genes exhibited either comparable or distinct expression patterns comparing to their Arabidopsis counterparts. These fi ndings indicate the existence of both functional conservation and functional divergence between PtCLEs and their AtCLE orthologues. Our results provide valuable resources for future functional investigations of these critical signaling molecules in woody plants. },
author = {Liu, Zhijun and Yang, Nan and Lv, Yanting and Pan, Lixia and Lv, Shuo and Han, Huibin and Wang, Guodong},
journal = {Plant Signaling & Behavior},
number = {6},
publisher = {Landes Bioscience},
title = {{The CLE gene family in Populus trichocarpa}},
doi = {10.1080/15592324.2016.1191734},
volume = {11},
year = {2016},
}
@inproceedings{1379,
abstract = {We investigate the complexity of finding an embedded non-orientable surface of Euler genus g in a triangulated 3-manifold. This problem occurs both as a natural question in low-dimensional topology, and as a first non-trivial instance of embeddability of complexes into 3-manifolds. We prove that the problem is NP-hard, thus adding to the relatively few hardness results that are currently known in 3-manifold topology. In addition, we show that the problem lies in NP when the Euler genus g is odd, and we give an explicit algorithm in this case.},
author = {Burton, Benjamin and De Mesmay, Arnaud N and Wagner, Uli},
location = {Medford, MA, USA},
pages = {24.1 -- 24.15},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing},
title = {{Finding non-orientable surfaces in 3-manifolds}},
doi = {10.4230/LIPIcs.SoCG.2016.24},
volume = {51},
year = {2016},
}
@article{1477,
abstract = {We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples.},
author = {Chatterjee, Krishnendu and Chmelik, Martin and Tracol, Mathieu},
journal = {Journal of Computer and System Sciences},
number = {5},
pages = {878 -- 911},
publisher = {Elsevier},
title = {{What is decidable about partially observable Markov decision processes with ω-regular objectives}},
doi = {10.1016/j.jcss.2016.02.009},
volume = {82},
year = {2016},
}
@article{1529,
abstract = {We consider partially observable Markov decision processes (POMDPs) with a set of target states and an integer cost associated with every transition. The optimization objective we study asks to minimize the expected total cost of reaching a state in the target set, 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, both double exponential in the POMDP state space size; (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 = {Chatterjee, Krishnendu and Chmelik, Martin and Gupta, Raghav and Kanodia, Ayush},
journal = {Artificial Intelligence},
pages = {26 -- 48},
publisher = {Elsevier},
title = {{Optimal cost almost-sure reachability in POMDPs}},
doi = {10.1016/j.artint.2016.01.007},
volume = {234},
year = {2016},
}
@misc{5451,
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
issn = {2664-1690},
pages = {34},
publisher = {IST Austria},
title = {{Strong amplifiers of natural selection}},
doi = {10.15479/AT:IST-2016-728-v1-1},
year = {2016},
}
@misc{5445,
abstract = {We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs. },
author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Velner, Yaron},
issn = {2664-1690},
pages = {33},
publisher = {IST Austria},
title = {{Quantitative interprocedural analysis}},
doi = {10.15479/AT:IST-2016-523-v1-1},
year = {2016},
}
@misc{5446,
abstract = {We study the problem of developing efficient approaches for proving termination of recursive programs with one-dimensional arrays. Ranking functions serve as a sound and complete approach for proving termination of non-recursive programs without array operations. First, we generalize ranking functions to the notion of measure functions, and prove that measure functions (i) provide a sound method to prove termination of recursive programs (with one-dimensional arrays), and (ii) is both sound and complete over recursive programs without array operations. Our second contribution is the synthesis of measure functions of specific forms in polynomial time. More precisely, we prove that (i) polynomial measure functions over recursive programs can be synthesized in polynomial time through Farkas’ Lemma and Handelman’s Theorem, and (ii) measure functions involving logarithm and exponentiation can be synthesized in polynomial time through abstraction of logarithmic or exponential terms and Handelman’s Theorem. A key application of our method is the worst-case analysis of recursive programs. While previous methods obtain worst-case polynomial bounds of the form O(n^k), where k is an integer, our polynomial time methods can synthesize bounds of the form O(n log n), as well as O(n^x), where x is not an integer. We show the applicability of our automated technique to obtain worst-case complexity of classical recursive algorithms such as (i) Merge-Sort, the divideand-
conquer algorithm for the Closest-Pair problem, where we obtain O(n log n) worst-case bound, and (ii) Karatsuba’s algorithm for polynomial multiplication and Strassen’s algorithm for matrix multiplication, where we obtain O(n^x) bound, where x is not an integer and close to the best-known bounds for the respective algorithms. Finally, we present experimental results to demonstrate the
effectiveness of our approach.},
author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3},
issn = {2664-1690},
pages = {26},
publisher = {IST Austria},
title = {{Termination and worst-case analysis of recursive programs}},
year = {2016},
}
@misc{5447,
abstract = {We consider the problem of developing automated techniques to aid the average-case complexity analysis of programs. Several classical textbook algorithms have quite efficient average-case complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPONCOLLECTOR). Since the main focus of average-case analysis is to obtain efficient bounds, we consider bounds that are either logarithmic,
linear, or almost-linear (O(log n), O(n), O(n · log n),
respectively, where n represents the size of the input). Our main contribution is a sound approach for deriving such average-case bounds for randomized recursive programs. Our approach is efficient (a simple linear-time algorithm), and it is based on (a) the analysis of recurrence relations induced by randomized algorithms, and (b) a guess-and-check technique. Our approach can infer the asymptotically optimal average-case bounds for classical randomized algorithms, including RANDOMIZED-SEARCH, QUICKSORT, QUICK-SELECT, COUPON-COLLECTOR, where the worstcase
bounds are either inefficient (such as linear as compared to logarithmic of average-case, or quadratic as compared to linear or almost-linear of average-case), or ineffective. We have implemented our approach, and the experimental results show that we obtain the bounds efficiently for various classical algorithms.},
author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3},
issn = {2664-1690},
pages = {20},
publisher = {IST Austria},
title = {{Average-case analysis of programs: Automated recurrence analysis for almost-linear bounds}},
year = {2016},
}
@article{1274,
abstract = {Synchronized tissue polarization during regeneration or de novo vascular tissue formation is a plant-specific example of intercellular communication and coordinated development. According to the canalization hypothesis, the plant hormone auxin serves as polarizing signal that mediates directional channel formation underlying the spatio-temporal vasculature patterning. A necessary part of canalization is a positive feedback between auxin signaling and polarity of the intercellular auxin flow. The cellular and molecular mechanisms of this process are still poorly understood, not the least, because of a lack of a suitable model system. We show that the main genetic model plant, Arabidopsis (Arabidopsis thaliana) can be used to study the canalization during vascular cambium regeneration and new vasculature formation. We monitored localized auxin responses, directional auxin-transport channels formation, and establishment of new vascular cambium polarity during regenerative processes after stem wounding. The increased auxin response above and around the wound preceded the formation of PIN1 auxin transporter-marked channels from the primarily homogenous tissue and the transient, gradual changes in PIN1 localization preceded the polarity of newly formed vascular tissue. Thus, Arabidopsis is a useful model for studies of coordinated tissue polarization and vasculature formation after wounding allowing for genetic and mechanistic dissection of the canalization hypothesis.},
author = {Mazur, Ewa and Benková, Eva and Friml, Jirí},
journal = {Scientific Reports},
publisher = {Nature Publishing Group},
title = {{Vascular cambium regeneration and vessel formation in wounded inflorescence stems of Arabidopsis}},
doi = {10.1038/srep33754},
volume = {6},
year = {2016},
}
@misc{5449,
abstract = {The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population.
The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure.
Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade.
In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively.},
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
issn = {2664-1690},
pages = {22},
publisher = {IST Austria},
title = {{Amplification on undirected population structures: Comets beat stars}},
doi = {10.15479/AT:IST-2016-648-v1-1},
year = {2016},
}
@misc{5453,
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
issn = {2664-1690},
pages = {34},
publisher = {IST Austria},
title = {{Arbitrarily strong amplifiers of natural selection}},
doi = {10.15479/AT:IST-2017-749-v3-1},
year = {2016},
}
@misc{5448,
abstract = {We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.
We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.
1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.
2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.},
author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3 and Anonymous, 4},
issn = {2664-1690},
pages = {20},
publisher = {IST Austria},
title = {{Data-centric dynamic partial order reduction}},
year = {2016},
}
@phdthesis{1398,
abstract = {Hybrid zones represent evolutionary laboratories, where recombination brings together alleles in combinations which have not previously been tested by selection. This provides an excellent opportunity to test the effect of molecular variation on fitness, and how this variation is able to spread through populations in a natural context. The snapdragon Antirrhinum majus is polymorphic in the wild for two loci controlling the distribution of yellow and magenta floral pigments. Where the yellow A. m. striatum and the magenta A. m. pseudomajus meet along a valley in the Spanish Pyrenees they form a stable hybrid zone Alleles at these loci recombine to give striking transgressive variation for flower colour. The sharp transition in phenotype over ~1km implies strong selection maintaining the hybrid zone. An indirect assay of pollinator visitation in the field found that pollinators forage in a positive-frequency dependent manner on Antirrhinum, matching previous data on fruit set. Experimental arrays and paternity analysis of wild-pollinated seeds demonstrated assortative mating for pigmentation alleles, and that pollinator behaviour alone is sufficient to explain this pattern. Selection by pollinators should be sufficiently strong to maintain the hybrid zone, although other mechanisms may be at work. At a broader scale I examined evolutionary transitions between yellow and anthocyanin pigmentation in the tribe Antirrhinae, and found that selection has acted strate that pollinators are a major determinant of reproductive success and mating patterns in wild Antirrhinum.},
author = {Ellis, Thomas},
pages = {130},
publisher = {IST Austria},
title = {{The role of pollinator-mediated selection in the maintenance of a flower color polymorphism in an Antirrhinum majus hybrid zone}},
doi = {10.15479/AT:ISTA:TH_526 },
year = {2016},
}
@misc{5551,
abstract = {Data from array experiments investigating pollinator behaviour on snapdragons in controlled conditions, and their effect on plant mating. Data were collected as part of Tom Ellis' PhD thesis , submitted February 2016.
We placed a total of 36 plants in a grid inside a closed organza tent, with a single hive of commercially bred bumblebees (Bombus hortorum). We used only the yellow-flowered Antirrhinum majus striatum and the magenta-flowered Antirrhinum majus pseudomajus, at ratios of 6:36, 12:24, 18:18, 24:12 and 30:6.
After 24 hours to learn how to deal with snapdragons, I observed pollinators foraging on plants, and recorded the transitions between plants. Thereafter seeds on plants were allowed to develops. A sample of these were grown to maturity when their flower colour could be determined, and they were scored as yellow, magenta, or hybrid.},
author = {Ellis, Thomas},
publisher = {IST Austria},
title = {{Data on pollinator observations and offpsring phenotypes}},
doi = {10.15479/AT:ISTA:35},
year = {2016},
}
@misc{5552,
abstract = {Data on pollinator visitation to wild snapdragons in a natural hybrid zone, collected as part of Tom Ellis' PhD thesis (submitted February 2016).
Snapdragon flowers have a mouth-like structure which pollinators must open to access nectar. We placed 5mm cellophane tags in these mouths, which are held in place by the pressure of the flower until a pollinator visits. When she opens the flower, the tag drops out, and one can infer a visit. We surveyed plants over multiple days in 2010, 2011 and 2012.
Also included are data on phenotypic and demographic variables which may be explanatory variables for pollinator visitation.},
author = {Ellis, Thomas},
publisher = {IST Austria},
title = {{Pollinator visitation data for wild Antirrhinum majus plants, with phenotypic and frequency data.}},
doi = {10.15479/AT:ISTA:36},
year = {2016},
}
@misc{5553,
abstract = {Genotypic, phenotypic and demographic data for 2128 wild snapdragons and 1127 open-pollinated progeny from a natural hybrid zone, collected as part of Tom Ellis' PhD thesis (submitted) February 2016).
Tissue samples were sent to LGC Genomics in Berlin for DNA extraction, and genotyping at 70 SNP markers by KASPR genotyping. 29 of these SNPs failed to amplify reliably, and have been removed from this dataset.
Other data were retreived from an online database of this population at www.antspec.org.},
author = {Field, David and Ellis, Thomas},
keywords = {paternity assignment, pedigree, matting patterns, assortative mating, Antirrhinum majus, frequency-dependent selection, plant-pollinator interaction},
publisher = {IST Austria},
title = {{Inference of mating patterns among wild snapdragons in a natural hybrid zone in 2012}},
doi = {10.15479/AT:ISTA:37},
year = {2016},
}
@misc{5550,
abstract = {We collected flower colour information on species in the tribe Antirrhineae from taxonomic literature. We also retreived molecular data from GenBank for as many of these species as possible to estimate phylogenetic relationships among these taxa. We then used the R package 'diversitree' to examine patterns of evolutionary transitions between anthocyanin and yellow pigmentation across the phylogeny.
For full details of the methods see:
Ellis TJ and Field DL "Repeated gains in yellow and anthocyanin pigmentation in flower colour transitions in the Antirrhineae”, Annals of Botany (in press)},
author = {Ellis, Thomas and Field, David},
publisher = {IST Austria},
title = {{Flower colour data and phylogeny (NEXUS) files}},
doi = {10.15479/AT:ISTA:34},
year = {2016},
}
@phdthesis{1122,
abstract = {Computer graphics is an extremely exciting field for two reasons. On the one hand,
there is a healthy injection of pragmatism coming from the visual effects industry
that want robust algorithms that work so they can produce results at an increasingly
frantic pace. On the other hand, they must always try to push the envelope and
achieve the impossible to wow their audiences in the next blockbuster, which means
that the industry has not succumb to conservatism, and there is plenty of room to
try out new and crazy ideas if there is a chance that it will pan into something
useful.
Water simulation has been in visual effects for decades, however it still remains
extremely challenging because of its high computational cost and difficult artdirectability.
The work in this thesis tries to address some of these difficulties.
Specifically, we make the following three novel contributions to the state-of-the-art
in water simulation for visual effects.
First, we develop the first algorithm that can convert any sequence of closed
surfaces in time into a moving triangle mesh. State-of-the-art methods at the time
could only handle surfaces with fixed connectivity, but we are the first to be able to
handle surfaces that merge and split apart. This is important for water simulation
practitioners, because it allows them to convert splashy water surfaces extracted
from particles or simulated using grid-based level sets into triangle meshes that can
be either textured and enhanced with extra surface dynamics as a post-process.
We also apply our algorithm to other phenomena that merge and split apart, such
as morphs and noisy reconstructions of human performances.
Second, we formulate a surface-based energy that measures the deviation of a
water surface froma physically valid state. Such discrepancies arise when there is a
mismatch in the degrees of freedom between the water surface and the underlying
physics solver. This commonly happens when practitioners use a moving triangle
mesh with a grid-based physics solver, or when high-resolution grid-based surfaces
are combined with low-resolution physics. Following the direction of steepest
descent on our surface-based energy, we can either smooth these artifacts or turn
them into high-resolution waves by interpreting the energy as a physical potential.
Third, we extend state-of-the-art techniques in non-reflecting boundaries to handle spatially and time-varying background flows. This allows a novel new
workflow where practitioners can re-simulate part of an existing simulation, such
as removing a solid obstacle, adding a new splash or locally changing the resolution.
Such changes can easily lead to new waves in the re-simulated region that would
reflect off of the new simulation boundary, effectively ruining the illusion of a
seamless simulation boundary between the existing and new simulations. Our
non-reflecting boundaries makes sure that such waves are absorbed.},
author = {Bojsen-Hansen, Morten},
pages = {114},
publisher = {IST Austria},
title = {{Tracking, correcting and absorbing water surface waves}},
doi = {10.15479/AT:ISTA:th_640},
year = {2016},
}
@misc{5557,
abstract = {Small synthetic discrete tomography problems.
Sizes are 32x32, 64z64 and 256x256.
Projection angles are 2, 4, and 6.
Number of labels are 3 and 5.},
author = {Swoboda, Paul},
keywords = {discrete tomography},
publisher = {IST Austria},
title = {{Synthetic discrete tomography problems}},
doi = {10.15479/AT:ISTA:46},
year = {2016},
}
@misc{5452,
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
issn = {2664-1690},
pages = {32},
publisher = {IST Austria},
title = {{Arbitrarily strong amplifiers of natural selection}},
doi = {10.15479/AT:IST-2017-728-v2-1},
year = {2016},
}
@misc{5554,
abstract = {The data stored here is used in Murat Tugrul's PhD thesis (Chapter 3), which is related to the evolution of bacterial RNA polymerase binding.
Magdalena Steinrueck (PhD Student in Calin Guet's group at IST Austria) performed the experiments and created the data on de novo promoter evolution. Fabienne Jesse (PhD Student in Jon Bollback's group at IST Austria) performed the experiments and created the data on lac promoter evolution.},
author = {Tugrul, Murat},
keywords = {RNAP binding, de novo promoter evolution, lac promoter},
publisher = {IST Austria},
title = {{Experimental Data for Binding Site Evolution of Bacterial RNA Polymerase}},
doi = {10.15479/AT:ISTA:43},
year = {2016},
}
@misc{5555,
abstract = {This FIJI script calculates the population average of the migration speed as a function of time of all cells from wide field microscopy movies.},
author = {Hauschild, Robert},
keywords = {cell migration, wide field microscopy, FIJI},
publisher = {IST Austria},
title = {{Fiji script to determine average speed and direction of migration of cells}},
doi = {10.15479/AT:ISTA:44},
year = {2016},
}
@misc{5558,
abstract = {PhD thesis LaTeX source code},
author = {Bojsen-Hansen, Morten},
publisher = {IST Austria},
title = {{Tracking, Correcting and Absorbing Water Surface Waves}},
doi = {10.15479/AT:ISTA:48},
year = {2016},
}
@inproceedings{1438,
abstract = {In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: (a) qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); (b) quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism.},
author = {Chatterjee, Krishnendu and Fu, Hongfei and Novotny, Petr and Hasheminezhad, Rouzbeh},
location = {St. Petersburg, FL, USA},
pages = {327 -- 342},
publisher = {ACM},
title = {{Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs}},
doi = {10.1145/2837614.2837639},
volume = {20-22},
year = {2016},
}
@inproceedings{1193,
abstract = {We consider the recent formulation of the Algorithmic Lovász Local Lemma [1], [2] for finding objects that avoid "bad features", or "flaws". It extends the Moser-Tardos resampling algorithm [3] to more general discrete spaces. At each step the method picks a flaw present in the current state and "resamples" it using a "resampling oracle" provided by the user. However, it is less flexible than the Moser-Tardos method since [1], [2] require a specific flaw selection rule, whereas [3] allows an arbitrary rule (and thus can potentially be implemented more efficiently). We formulate a new "commutativity" condition, and prove that it is sufficient for an arbitrary rule to work. It also enables an efficient parallelization under an additional assumption. We then show that existing resampling oracles for perfect matchings and permutations do satisfy this condition. Finally, we generalize the precondition in [2] (in the case of symmetric potential causality graphs). This unifies special cases that previously were treated separately.},
author = {Kolmogorov, Vladimir},
booktitle = {Proceedings - Annual IEEE Symposium on Foundations of Computer Science},
location = {New Brunswick, NJ, USA },
publisher = {IEEE},
title = {{Commutativity in the algorithmic Lovasz local lemma}},
doi = {10.1109/FOCS.2016.88},
volume = {2016-December},
year = {2016},
}
@article{1358,
abstract = {Gene regulation relies on the specificity of transcription factor (TF)–DNA interactions. Limited specificity may lead to crosstalk: a regulatory state in which a gene is either incorrectly activated due to noncognate TF–DNA interactions or remains erroneously inactive. As each TF can have numerous interactions with noncognate cis-regulatory elements, crosstalk is inherently a global problem, yet has previously not been studied as such. We construct a theoretical framework to analyse the effects of global crosstalk on gene regulation. We find that crosstalk presents a significant challenge for organisms with low-specificity TFs, such as metazoans. Crosstalk is not easily mitigated by known regulatory schemes acting at equilibrium, including variants of cooperativity and combinatorial regulation. Our results suggest that crosstalk imposes a previously unexplored global constraint on the functioning and evolution of regulatory networks, which is qualitatively distinct from the known constraints that act at the level of individual gene regulatory elements.},
author = {Friedlander, Tamar and Prizak, Roshan and Guet, Calin C and Barton, Nicholas H and Tkacik, Gasper},
journal = {Nature Communications},
publisher = {Nature Publishing Group},
title = {{Intrinsic limits to gene regulation by global crosstalk}},
doi = {10.1038/ncomms12307},
volume = {7},
year = {2016},
}
@inproceedings{1341,
abstract = {In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.},
author = {Avni, Guy and Henzinger, Thomas A and Kupferman, Orna},
location = {Liverpool, United Kingdom},
pages = {153 -- 166},
publisher = {Springer},
title = {{Dynamic resource allocation games}},
doi = {10.1007/978-3-662-53354-3_13},
volume = {9928},
year = {2016},
}
@article{1346,
abstract = {ATP production requires the establishment of an electrochemical proton gradient across the inner mitochondrial membrane. Mitochondrial uncouplers dissipate this proton gradient and disrupt numerous cellular processes, including vesicular trafficking, mainly through energy depletion. Here we show that Endosidin9 (ES9), a novel mitochondrial uncoupler, is a potent inhibitor of clathrin-mediated endocytosis (CME) in different systems and that ES9 induces inhibition of CME not because of its effect on cellular ATP, but rather due to its protonophore activity that leads to cytoplasm acidification. We show that the known tyrosine kinase inhibitor tyrphostinA23, which is routinely used to block CME, displays similar properties, thus questioning its use as a specific inhibitor of cargo recognition by the AP-2 adaptor complex via tyrosine motif-based endocytosis signals. Furthermore, we show that cytoplasm acidification dramatically affects the dynamics and recruitment of clathrin and associated adaptors, and leads to reduction of phosphatidylinositol 4,5-biphosphate from the plasma membrane.},
author = {Dejonghe, Wim and Kuenen, Sabine and Mylle, Evelien and Vasileva, Mina K and Keech, Olivier and Viotti, Corrado and Swerts, Jef and Fendrych, Matyas and Ortiz Morea, Fausto and Mishev, Kiril and Delang, Simon and Scholl, Stefan and Zarza, Xavier and Heilmann, Mareike and Kourelis, Jiorgos and Kasprowicz, Jaroslaw and Nguyen, Le and Drozdzecki, Andrzej and Van Houtte, Isabelle and Szatmári, Anna and Majda, Mateusz and Baisa, Gary and Bednarek, Sebastian and Robert, Stéphanie and Audenaert, Dominique and Testerink, Christa and Munnik, Teun and Van Damme, Daniël and Heilmann, Ingo and Schumacher, Karin and Winne, Johan and Friml, Jirí and Verstreken, Patrik and Russinova, Eugenia},
journal = {Nature Communications},
publisher = {Nature Publishing Group},
title = {{Mitochondrial uncouplers inhibit clathrin-mediated endocytosis largely through cytoplasmic acidification}},
doi = {10.1038/ncomms11710},
volume = {7},
year = {2016},
}
@inproceedings{1165,
abstract = {We show that c-planarity is solvable in quadratic time for flat clustered graphs with three clusters if the combinatorial embedding of the underlying graph is fixed. In simpler graph-theoretical terms our result can be viewed as follows. Given a graph G with the vertex set partitioned into three parts embedded on a 2-sphere, our algorithm decides if we can augment G by adding edges without creating an edge-crossing so that in the resulting spherical graph the vertices of each part induce a connected sub-graph. We proceed by a reduction to the problem of testing the existence of a perfect matching in planar bipartite graphs. We formulate our result in a slightly more general setting of cyclic clustered graphs, i.e., the simple graph obtained by contracting each cluster, where we disregard loops and multi-edges, is a cycle.},
author = {Fulek, Radoslav},
location = {Athens, Greece},
pages = {94 -- 106},
publisher = {Springer},
title = {{C-planarity of embedded cyclic c-graphs}},
doi = {10.1007/978-3-319-50106-2_8},
volume = {9801 },
year = {2016},
}
@inproceedings{1071,
abstract = {We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. },
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
location = {Aarhus, Denmark},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik},
title = {{Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs}},
doi = {10.4230/LIPIcs.ESA.2016.28},
volume = {57},
year = {2016},
}
@inproceedings{1229,
abstract = {Witness encryption (WE) was introduced by Garg et al. [GGSW13]. A WE scheme is defined for some NP language L and lets a sender encrypt messages relative to instances x. A ciphertext for x can be decrypted using w witnessing x ∈ L, but hides the message if x ∈ L. Garg et al. construct WE from multilinear maps and give another construction [GGH+13b] using indistinguishability obfuscation (iO) for circuits. Due to the reliance on such heavy tools, WE can cur- rently hardly be implemented on powerful hardware and will unlikely be realizable on constrained devices like smart cards any time soon. We construct a WE scheme where encryption is done by simply computing a Naor-Yung ciphertext (two CPA encryptions and a NIZK proof). To achieve this, our scheme has a setup phase, which outputs public parameters containing an obfuscated circuit (only required for decryption), two encryption keys and a common reference string (used for encryption). This setup need only be run once, and the parame- ters can be used for arbitrary many encryptions. Our scheme can also be turned into a functional WE scheme, where a message is encrypted w.r.t. a statement and a function f, and decryption with a witness w yields f (m, w). Our construction is inspired by the functional encryption scheme by Garg et al. and we prove (selective) security assuming iO and statistically simulation-sound NIZK. We give a construction of the latter in bilinear groups and combining it with ElGamal encryption, our ciphertexts are of size 1.3 kB at a 128-bit security level and can be computed on a smart card.},
author = {Abusalah, Hamza M and Fuchsbauer, Georg and Pietrzak, Krzysztof Z},
location = {Guildford, UK},
pages = {285 -- 303},
publisher = {Springer},
title = {{Offline witness encryption}},
doi = {10.1007/978-3-319-39555-5_16},
volume = {9696},
year = {2016},
}
@inproceedings{1236,
abstract = {A constrained pseudorandom function F: K × X → Y for a family T ⊆ 2X of subsets of X is a function where for any key k ∈ K and set S ∈ T one can efficiently compute a constrained key kS which allows to evaluate F (k, ·) on all inputs x ∈ S, while even given this key, the outputs on all inputs x ∉ S look random. At Asiacrypt’13 Boneh and Waters gave a construction which supports the most general set family so far. Its keys kc are defined for sets decided by boolean circuits C and enable evaluation of the PRF on any x ∈ X where C(x) = 1. In their construction the PRF input length and the size of the circuits C for which constrained keys can be computed must be fixed beforehand during key generation. We construct a constrained PRF that has an unbounded input length and whose constrained keys can be defined for any set recognized by a Turing machine. The only a priori bound we make is on the description size of the machines. We prove our construction secure assuming publiccoin differing-input obfuscation. As applications of our constrained PRF we build a broadcast encryption scheme where the number of potential receivers need not be fixed at setup (in particular, the length of the keys is independent of the number of parties) and the first identity-based non-interactive key exchange protocol with no bound on the number of parties that can agree on a shared key.},
author = {Abusalah, Hamza M and Fuchsbauer, Georg and Pietrzak, Krzysztof Z},
location = {San Francisco, CA, USA},
pages = {413 -- 428},
publisher = {Springer},
title = {{Constrained PRFs for unbounded inputs}},
doi = {10.1007/978-3-319-29485-8_24},
volume = {9610},
year = {2016},
}
@inproceedings{1235,
abstract = {A constrained pseudorandom function (CPRF) F: K×X → Y for a family T of subsets of χ is a function where for any key k ∈ K and set S ∈ T one can efficiently compute a short constrained key kS, which allows to evaluate F(k, ·) on all inputs x ∈ S, while the outputs on all inputs x /∈ S look random even given kS. Abusalah et al. recently constructed the first constrained PRF for inputs of arbitrary length whose sets S are decided by Turing machines. They use their CPRF to build broadcast encryption and the first ID-based non-interactive key exchange for an unbounded number of users. Their constrained keys are obfuscated circuits and are therefore large. In this work we drastically reduce the key size and define a constrained key for a Turing machine M as a short signature on M. For this, we introduce a new signature primitive with constrained signing keys that let one only sign certain messages, while forging a signature on others is hard even when knowing the coins for key generation.},
author = {Abusalah, Hamza M and Fuchsbauer, Georg},
location = {Guildford, UK},
pages = {445 -- 463},
publisher = {Springer},
title = {{Constrained PRFs for unbounded inputs with short keys}},
doi = {10.1007/978-3-319-39555-5_24},
volume = {9696},
year = {2016},
}
@article{1100,
abstract = {During metazoan development, the temporal pattern of morphogen signaling is critical for organizing cell fates in space and time. Yet, tools for temporally controlling morphogen signaling within the embryo are still scarce. Here, we developed a photoactivatable Nodal receptor to determine how the temporal pattern of Nodal signaling affects cell fate specification during zebrafish gastrulation. By using this receptor to manipulate the duration of Nodal signaling in vivo by light, we show that extended Nodal signaling within the organizer promotes prechordal plate specification and suppresses endoderm differentiation. Endoderm differentiation is suppressed by extended Nodal signaling inducing expression of the transcriptional repressor goosecoid (gsc) in prechordal plate progenitors, which in turn restrains Nodal signaling from upregulating the endoderm differentiation gene sox17 within these cells. Thus, optogenetic manipulation of Nodal signaling identifies a critical role of Nodal signaling duration for organizer cell fate specification during gastrulation.},
author = {Sako, Keisuke and Pradhan, Saurabh and Barone, Vanessa and Inglés Prieto, Álvaro and Mueller, Patrick and Ruprecht, Verena and Capek, Daniel and Galande, Sanjeev and Janovjak, Harald L and Heisenberg, Carl-Philipp J},
journal = {Cell Reports},
number = {3},
pages = {866 -- 877},
publisher = {Cell Press},
title = {{Optogenetic control of nodal signaling reveals a temporal pattern of nodal signaling regulating cell fate specification during gastrulation}},
doi = {10.1016/j.celrep.2016.06.036},
volume = {16},
year = {2016},
}
@inproceedings{1378,
abstract = {We give a detailed and easily accessible proof of Gromov's Topological Overlap Theorem. Let X be a finite simplicial complex or, more generally, a finite polyhedral cell complex of dimension d. Informally, the theorem states that if X has sufficiently strong higher-dimensional expansion properties (which generalize edge expansion of graphs and are defined in terms of cellular cochains of X) then X has the following topological overlap property: for every continuous map X → ℝd there exists a point p ∈ ℝd whose preimage intersects a positive fraction μ > 0 of the d-cells of X. More generally, the conclusion holds if ℝd is replaced by any d-dimensional piecewise-linear (PL) manifold M, with a constant μ that depends only on d and on the expansion properties of X, but not on M.},
author = {Dotterrer, Dominic and Kaufman, Tali and Wagner, Uli},
location = {Medford, MA, USA},
pages = {35.1 -- 35.10},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing},
title = {{On expansion and topological overlap}},
doi = {10.4230/LIPIcs.SoCG.2016.35},
volume = {51},
year = {2016},
}
@article{1328,
abstract = {Hole spins have gained considerable interest in the past few years due to their potential for fast electrically controlled qubits. Here, we study holes confined in Ge hut wires, a so-far unexplored type of nanostructure. Low-temperature magnetotransport measurements reveal a large anisotropy between the in-plane and out-of-plane g-factors of up to 18. Numerical simulations verify that this large anisotropy originates from a confined wave function of heavy-hole character. A light-hole admixture of less than 1% is estimated for the states of lowest energy, leading to a surprisingly large reduction of the out-of-plane g-factors compared with those for pure heavy holes. Given this tiny light-hole contribution, the spin lifetimes are expected to be very long, even in isotopically nonpurified samples.},
author = {Watzinger, Hannes and Kloeffel, Christoph and Vukusic, Lada and Rossell, Marta and Sessi, Violetta and Kukucka, Josip and Kirchschlager, Raimund and Lausecker, Elisabeth and Truhlar, Alisha and Glaser, Martin and Rastelli, Armando and Fuhrer, Andreas and Loss, Daniel and Katsaros, Georgios},
journal = {Nano Letters},
number = {11},
pages = {6879 -- 6885},
publisher = {American Chemical Society},
title = {{Heavy-hole states in germanium hut wires}},
doi = {10.1021/acs.nanolett.6b02715},
volume = {16},
year = {2016},
}
@inproceedings{8094,
abstract = {With the accelerated development of robot technologies, optimal control becomes one of the central themes of research. In traditional approaches, the controller, by its internal functionality, finds appropriate actions on the basis of the history of sensor values, guided by the goals, intentions, objectives, learning schemes, and so forth. The idea is that the controller controls the world---the body plus its environment---as reliably as possible. This paper focuses on new lines of self-organization for developmental robotics. We apply the recently developed differential extrinsic synaptic plasticity to a muscle-tendon driven arm-shoulder system from the Myorobotics toolkit. In the experiments, we observe a vast variety of self-organized behavior patterns: when left alone, the arm realizes pseudo-random sequences of different poses. By applying physical forces, the system can be entrained into definite motion patterns like wiping a table. Most interestingly, after attaching an object, the controller gets in a functional resonance with the object's internal dynamics, starting to shake spontaneously bottles half-filled with water or sensitively driving an attached pendulum into a circular mode. When attached to the crank of a wheel the neural system independently discovers how to rotate it. In this way, the robot discovers affordances of objects its body is interacting with.},
author = {Martius, Georg S and Hostettler, Rafael and Knoll, Alois and Der, Ralf},
booktitle = {Proceedings of the Artificial Life Conference 2016},
isbn = {9780262339360},
location = {Cancun, Mexico},
pages = {142--143},
publisher = {MIT Press},
title = {{Self-organized control of an tendon driven arm by differential extrinsic plasticity}},
doi = {10.7551/978-0-262-33936-0-ch029},
volume = {28},
year = {2016},
}
@inproceedings{1362,
abstract = {We present a boundary element based method for fast simulation of brittle fracture. By introducing simplifying assumptions that allow us to quickly estimate stress intensities and opening displacements during crack propagation, we build a fracture algorithm where the cost of each time step scales linearly with the length of the crackfront. The transition from a full boundary element method to our faster variant is possible at the beginning of any time step. This allows us to build a hybrid method, which uses the expensive but more accurate BEM while the number of degrees of freedom is low, and uses the fast method once that number exceeds a given threshold as the crack geometry becomes more complicated. Furthermore, we integrate this fracture simulation with a standard rigid-body solver. Our rigid-body coupling solves a Neumann boundary value problem by carefully separating translational, rotational and deformational components of the collision forces and then applying a Tikhonov regularizer to the resulting linear system. We show that our method produces physically reasonable results in standard test cases and is capable of dealing with complex scenes faster than previous finite- or boundary element approaches.},
author = {Hahn, David and Wojtan, Christopher J},
location = {Anaheim, CA, USA},
number = {4},
publisher = {ACM},
title = {{Fast approximations for boundary element based brittle fracture simulation}},
doi = {10.1145/2897824.2925902},
volume = {35},
year = {2016},
}
@misc{5556,
abstract = {MATLAB code and processed datasets available for reproducing the results in:
Lukačišin, M.*, Landon, M.*, Jajoo, R*. (2016) Sequence-Specific Thermodynamic Properties of Nucleic Acids Influence Both Transcriptional Pausing and Backtracking in Yeast.
*equal contributions},
author = {Lukacisin, Martin and Landon, Matthieu and Jajoo, Rishi},
keywords = {transcription, pausing, backtracking, polymerase, RNA, NET-seq, nucleosome, basepairing},
publisher = {IST Austria},
title = {{MATLAB analysis code for 'Sequence-Specific Thermodynamic Properties of Nucleic Acids Influence Both Transcriptional Pausing and Backtracking in Yeast'}},
doi = {10.15479/AT:ISTA:45},
year = {2016},
}
@inproceedings{1437,
abstract = {We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.},
author = {Chatterjee, Krishnendu and Goharshady, Amir and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
location = {St. Petersburg, FL, USA},
pages = {733 -- 747},
publisher = {ACM},
title = {{Algorithms for algebraic path properties in concurrent systems of constant treewidth components}},
doi = {10.1145/2837614.2837624},
volume = {20-22},
year = {2016},
}
@inproceedings{1386,
abstract = {We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz's, yielding an efficient method which is not only sound, but also semi-complete over a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient quadratic ranking-supermartingales when a linear one does not exist even for simple affine programs.},
author = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir},
location = {Toronto, Canada},
pages = {3 -- 22},
publisher = {Springer},
title = {{Termination analysis of probabilistic programs through Positivstellensatz's}},
doi = {10.1007/978-3-319-41528-4_1},
volume = {9779},
year = {2016},
}
@article{1383,
abstract = {In plants, vacuolar H+-ATPase (V-ATPase) activity acidifies both the trans-Golgi network/early endosome (TGN/EE) and the vacuole. This dual V-ATPase function has impeded our understanding of how the pH homeostasis within the plant TGN/EE controls exo- and endocytosis. Here, we show that the weak V-ATPase mutant deetiolated3 (det3) displayed a pH increase in the TGN/EE, but not in the vacuole, strongly impairing secretion and recycling of the brassinosteroid receptor and the cellulose synthase complexes to the plasma membrane, in contrast to mutants lacking tonoplast-localized V-ATPase activity only. The brassinosteroid insensitivity and the cellulose deficiency defects in det3 were tightly correlated with reduced Golgi and TGN/EE motility. Thus, our results provide strong evidence that acidification of the TGN/EE, but not of the vacuole, is indispensable for functional secretion and recycling in plants.},
author = {Yu, Luo and Scholl, Stefan and Doering, Anett and Yi, Zhang and Irani, Niloufer and Di Rubbo, Simone and Neumetzler, Lutz and Krishnamoorthy, Praveen and Van Houtte, Isabelle and Mylle, Evelien and Bischoff, Volker and Vernhettes, Samantha and Winne, Johan and Friml, Jirí and Stierhof, York and Schumacher, Karin and Persson, Staffan and Russinova, Eugenia},
journal = {Nature Plants},
number = {7},
publisher = {Nature Publishing Group},
title = {{V-ATPase activity in the TGN/EE is required for exocytosis and recycling in Arabidopsis}},
doi = {10.1038/nplants.2015.94},
volume = {1},
year = {2015},
}
@inproceedings{1424,
abstract = {We consider the problem of statistical computations with persistence diagrams, a summary representation of topological features in data. These diagrams encode persistent homology, a widely used invariant in topological data analysis. While several avenues towards a statistical treatment of the diagrams have been explored recently, we follow an alternative route that is motivated by the success of methods based on the embedding of probability measures into reproducing kernel Hilbert spaces. In fact, a positive definite kernel on persistence diagrams has recently been proposed, connecting persistent homology to popular kernel-based learning techniques such as support vector machines. However, important properties of that kernel enabling a principled use in the context of probability measure embeddings remain to be explored. Our contribution is to close this gap by proving universality of a variant of the original kernel, and to demonstrate its effective use in twosample hypothesis testing on synthetic as well as real-world data.},
author = {Kwitt, Roland and Huber, Stefan and Niethammer, Marc and Lin, Weili and Bauer, Ulrich},
location = {Montreal, Canada},
pages = {3070 -- 3078},
publisher = {Neural Information Processing Systems},
title = {{Statistical topological data analysis-A kernel perspective}},
volume = {28},
year = {2015},
}
@inproceedings{1425,
abstract = {In this work we aim at extending the theoretical foundations of lifelong learning. Previous work analyzing this scenario is based on the assumption that learning tasks are sampled i.i.d. from a task environment or limited to strongly constrained data distributions. Instead, we study two scenarios when lifelong learning is possible, even though the observed tasks do not form an i.i.d. sample: first, when they are sampled from the same environment, but possibly with dependencies, and second, when the task environment is allowed to change over time in a consistent way. In the first case we prove a PAC-Bayesian theorem that can be seen as a direct generalization of the analogous previous result for the i.i.d. case. For the second scenario we propose to learn an inductive bias in form of a transfer procedure. We present a generalization bound and show on a toy example how it can be used to identify a beneficial transfer algorithm.},
author = {Pentina, Anastasia and Lampert, Christoph},
location = {Montreal, Canada},
pages = {1540 -- 1548},
publisher = {Neural Information Processing Systems},
title = {{Lifelong learning with non-i.i.d. tasks}},
volume = {2015},
year = {2015},
}
@inproceedings{1430,
abstract = {Evolutionary algorithms (EAs) form a popular optimisation paradigm inspired by natural evolution. In recent years the field of evolutionary computation has developed a rigorous analytical theory to analyse their runtime on many illustrative problems. Here we apply this theory to a simple model of natural evolution. In the Strong Selection Weak Mutation (SSWM) evolutionary regime the time between occurrence of new mutations is much longer than the time it takes for a new beneficial mutation to take over the population. In this situation, the population only contains copies of one genotype and evolution can be modelled as a (1+1)-type process where the probability of accepting a new genotype (improvements or worsenings) depends on the change in fitness. We present an initial runtime analysis of SSWM, quantifying its performance for various parameters and investigating differences to the (1+1) EA. We show that SSWM can have a moderate advantage over the (1+1) EA at crossing fitness valleys and study an example where SSWM outperforms the (1+1) EA by taking advantage of information on the fitness gradient.},
author = {Paixao, Tiago and Sudholt, Dirk and Heredia, Jorge and Trubenova, Barbora},
booktitle = {Proceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation},
location = {Madrid, Spain},
pages = {1455 -- 1462},
publisher = {ACM},
title = {{First steps towards a runtime comparison of natural and artificial evolution}},
doi = {10.1145/2739480.2754758},
year = {2015},
}
@inproceedings{1474,
abstract = {Cryptographic access control offers selective access to encrypted data via a combination of key management and functionality-rich cryptographic schemes, such as attribute-based encryption. Using this approach, publicly available meta-data may inadvertently leak information on the access policy that is enforced by cryptography, which renders cryptographic access control unusable in settings where this information is highly sensitive. We begin to address this problem by presenting rigorous definitions for policy privacy in cryptographic access control. For concreteness we set our results in the model of Role-Based Access Control (RBAC), where we identify and formalize several different flavors of privacy, however, our framework should serve as inspiration for other models of access control. Based on our insights we propose a new system which significantly improves on the privacy properties of state-of-the-art constructions. Our design is based on a novel type of privacy-preserving attribute-based encryption, which we introduce and show how to instantiate. We present our results in the context of a cryptographic RBAC system by Ferrara et al. (CSF'13), which uses cryptography to control read access to files, while write access is still delegated to trusted monitors. We give an extension of the construction that permits cryptographic control over write access. Our construction assumes that key management uses out-of-band channels between the policy enforcer and the users but eliminates completely the need for monitoring read/write access to the data.},
author = {Ferrara, Anna and Fuchsbauer, Georg and Liu, Bin and Warinschi, Bogdan},
location = {Verona, Italy},
pages = {46--60},
publisher = {IEEE},
title = {{Policy privacy in cryptographic access control}},
doi = {10.1109/CSF.2015.11},
year = {2015},
}