@misc{5377,
abstract = {Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and ω-regular objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean-payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two- player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP- hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two- player pushdown games. Finally we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.},
author = {Chatterjee, Krishnendu and Velner, Yaron},
issn = {2664-1690},
pages = {33},
publisher = {IST Austria},
title = {{Mean-payoff pushdown games}},
doi = {10.15479/AT:IST-2012-0002},
year = {2012},
}
@misc{5378,
abstract = {One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.},
author = {Chatterjee, Krishnendu and Chaubal, Siddhesh and Kamath, Pritish},
issn = {2664-1690},
pages = {21},
publisher = {IST Austria},
title = {{Faster algorithms for alternating refinement relations}},
doi = {10.15479/AT:IST-2012-0001},
year = {2012},
}
@misc{5396,
abstract = {We consider the problem of inference in agraphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pair-wise terms over a discretized domain. This allows the use of techniques originally devel-oped for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can out-perform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions.},
author = {Korc, Filip and Kolmogorov, Vladimir and Lampert, Christoph},
issn = {2664-1690},
pages = {13},
publisher = {IST Austria},
title = {{Approximating marginals using discrete energy minimization}},
doi = {10.15479/AT:IST-2012-0003},
year = {2012},
}
@techreport{5398,
abstract = {This document is created as a part of the project “Repository for Research Data on IST Austria”. It summarises the actual state of research data at IST Austria, based on survey results. It supports the choice of appropriate software, which would best fit the requirements of their users, the researchers.},
author = {Porsche, Jana},
publisher = {IST Austria},
title = {{Actual state of research data @ ISTAustria}},
year = {2012},
}
@inbook{5745,
author = {Gupta, Ashutosh},
booktitle = {Automated Technology for Verification and Analysis},
isbn = {9783642333859},
issn = {0302-9743},
location = {Thiruvananthapuram, Kerala, India},
pages = {107--121},
publisher = {Springer Berlin Heidelberg},
title = {{Improved Single Pass Algorithms for Resolution Proof Reduction}},
doi = {10.1007/978-3-642-33386-6_10},
volume = {7561},
year = {2012},
}
@article{6588,
abstract = {First we note that the best polynomial approximation to vertical bar x vertical bar on the set, which consists of an interval on the positive half-axis and a point on the negative half-axis, can be given by means of the classical Chebyshev polynomials. Then we explore the cases when a solution of the related problem on two intervals can be given in elementary functions.},
author = {Pausinger, Florian},
issn = {1812-9471},
journal = {Journal of Mathematical Physics, Analysis, Geometry},
number = {1},
pages = {63--78},
publisher = {B. Verkin Institute for Low Temperature Physics and Engineering},
title = {{Elementary solutions of the Bernstein problem on two intervals}},
volume = {8},
year = {2012},
}
@inproceedings{1384,
abstract = {Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition Ψ - usually a state predicate - such that the program satisfies the specification under the condition Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.},
author = {Beyer, Dirk and Henzinger, Thomas A and Keremoglu, Mehmet and Wendler, Philipp},
booktitle = {Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering},
location = {Cary, NC, USA},
publisher = {ACM},
title = {{Conditional model checking: A technique to pass information between verifiers}},
doi = {10.1145/2393596.2393664},
year = {2012},
}
@article{3836,
abstract = {Hierarchical Timing Language (HTL) is a coordination language for distributed, hard real-time applications. HTL is a hierarchical extension of Giotto and, like its predecessor, based on the logical execution time (LET) paradigm of real-time programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine (or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram structure needs to be flattened; the flattening makes separatecompilation difficult, and may result in E machinecode of exponential size. In this paper, we propose a generalization of the E machine, which supports a hierarchicalprogram structure at runtime through real-time trigger mechanisms that are arranged in a tree. We present the generalized E machine, and a modular compiler for HTL that generates code of linear size. The compiler may generate code for any part of a given HTL program separately in any order.},
author = {Ghosal, Arkadeb and Iercan, Daniel and Kirsch, Christoph and Henzinger, Thomas A and Sangiovanni Vincentelli, Alberto},
journal = {Science of Computer Programming},
number = {2},
pages = {96 -- 112},
publisher = {Elsevier},
title = {{Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code}},
doi = {10.1016/j.scico.2010.06.004},
volume = {77},
year = {2012},
}
@article{3846,
abstract = {We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A},
journal = {Journal of Computer and System Sciences},
number = {2},
pages = {394 -- 413},
publisher = {Elsevier},
title = {{A survey of stochastic ω regular games}},
doi = {10.1016/j.jcss.2011.05.002},
volume = {78},
year = {2012},
}
@article{3115,
abstract = {We consider the offset-deconstruction problem: Given a polygonal shape Q with n vertices, can it be expressed, up to a tolerance ε in Hausdorff distance, as the Minkowski sum of another polygonal shape P with a disk of fixed radius? If it does, we also seek a preferably simple-looking solution P; then, P's offset constitutes an accurate, vertex-reduced, and smoothened approximation of Q. We give an O(nlogn)-time exact decision algorithm that handles any polygonal shape, assuming the real-RAM model of computation. A variant of the algorithm, which we have implemented using the cgal library, is based on rational arithmetic and answers the same deconstruction problem up to an uncertainty parameter δ its running time additionally depends on δ. If the input shape is found to be approximable, this algorithm also computes an approximate solution for the problem. It also allows us to solve parameter-optimization problems induced by the offset-deconstruction problem. For convex shapes, the complexity of the exact decision algorithm drops to O(n), which is also the time required to compute a solution P with at most one more vertex than a vertex-minimal one.},
author = {Berberich, Eric and Halperin, Dan and Kerber, Michael and Pogalnikova, Roza},
journal = {Discrete & Computational Geometry},
number = {4},
pages = {964 -- 989},
publisher = {Springer},
title = {{Deconstructing approximate offsets}},
doi = {10.1007/s00454-012-9441-5},
volume = {48},
year = {2012},
}
@article{3117,
abstract = {We consider the problem of minimizing a function represented as a sum of submodular terms. We assume each term allows an efficient computation of exchange capacities. This holds, for example, for terms depending on a small number of variables, or for certain cardinality-dependent terms. A naive application of submodular minimization algorithms would not exploit the existence of specialized exchange capacity subroutines for individual terms. To overcome this, we cast the problem as a submodular flow (SF) problem in an auxiliary graph in such a way that applying most existing SF algorithms would rely only on these subroutines. We then explore in more detail Iwata's capacity scaling approach for submodular flows (Iwata 1997 [19]). In particular, we show how to improve its complexity in the case when the function contains cardinality-dependent terms.},
author = {Kolmogorov, Vladimir},
journal = {Discrete Applied Mathematics},
number = {15},
pages = {2246 -- 2258},
publisher = {Elsevier},
title = {{Minimizing a sum of submodular functions}},
doi = {10.1016/j.dam.2012.05.025},
volume = {160},
year = {2012},
}
@article{3118,
abstract = {We present a method for recovering a temporally coherent, deforming triangle mesh with arbitrarily changing topology from an incoherent sequence of static closed surfaces. We solve this problem using the surface geometry alone, without any prior information like surface templates or velocity fields. Our system combines a proven strategy for triangle mesh improvement, a robust multi-resolution non-rigid registration routine, and a reliable technique for changing surface mesh topology. We also introduce a novel topological constraint enforcement algorithm to ensure that the output and input always have similar topology. We apply our technique to a series of diverse input data from video reconstructions, physics simulations, and artistic morphs. The structured output of our algorithm allows us to efficiently track information like colors and displacement maps, recover velocity information, and solve PDEs on the mesh as a post process.},
author = {Bojsen-Hansen, Morten and Li, Hao and Wojtan, Christopher J},
journal = {ACM Transactions on Graphics},
number = {4},
publisher = {ACM},
title = {{Tracking surfaces with evolving topology}},
doi = {10.1145/2185520.2185549},
volume = {31},
year = {2012},
}
@inproceedings{3119,
abstract = {We present an approach for artist-directed animation of liquids using multiple levels of control over the simulation, ranging from the overall tracking of desired shapes to highly detailed secondary effects such as dripping streams, separating sheets of fluid, surface waves and ripples. The first portion of our technique is a volume preserving morph that allows the animator to produce a plausible fluid-like motion from a sparse set of control meshes. By rasterizing the resulting control meshes onto the simulation grid, the mesh velocities act as boundary conditions during the projection step of the fluid simulation. We can then blend this motion together with uncontrolled fluid velocities to achieve a more relaxed control over the fluid that captures natural inertial effects. Our method can produce highly detailed liquid surfaces with control over sub-grid details by using a mesh-based surface tracker on top of a coarse grid-based fluid simulation. We can create ripples and waves on the fluid surface attracting the surface mesh to the control mesh with spring-like forces and also by running a wave simulation over the surface mesh. Our video results demonstrate how our control scheme can be used to create animated characters and shapes that are made of water.
},
author = {Raveendran, Karthik and Thuerey, Nils and Wojtan, Christopher J and Turk, Greg},
booktitle = {Proceedings of the ACM SIGGRAPH/Eurographics Symposium on Computer Animation},
location = {Aire-la-Ville, Switzerland},
pages = {255 -- 264},
publisher = {ACM},
title = {{Controlling liquids using meshes}},
year = {2012},
}
@article{3120,
abstract = {We introduce a strategy based on Kustin-Miller unprojection that allows us to construct many hundreds of Gorenstein codimension 4 ideals with 9 × 16 resolutions (that is, nine equations and sixteen first syzygies). Our two basic games are called Tom and Jerry; the main application is the biregular construction of most of the anticanonically polarised Mori Fano 3-folds of Altinok's thesis. There are 115 cases whose numerical data (in effect, the Hilbert series) allow a Type I projection. In every case, at least one Tom and one Jerry construction works, providing at least two deformation families of quasismooth Fano 3-folds having the same numerics but different topology. © 2012 Copyright Foundation Compositio Mathematica.},
author = {Brown, Gavin and Kerber, Michael and Reid, Miles},
journal = {Compositio Mathematica},
number = {4},
pages = {1171 -- 1194},
publisher = {Cambridge University Press},
title = {{Fano 3 folds in codimension 4 Tom and Jerry Part I}},
doi = {10.1112/S0010437X11007226},
volume = {148},
year = {2012},
}
@article{3121,
abstract = {Voltage-activated Ca(2+) channels (VACCs) mediate Ca(2+) influx to trigger action potential-evoked neurotransmitter release, but the mechanism by which Ca(2+) regulates spontaneous transmission is unclear. We found that VACCs are the major physiological triggers for spontaneous release at mouse neocortical inhibitory synapses. Moreover, despite the absence of a synchronizing action potential, we found that spontaneous fusion of a GABA-containing vesicle required the activation of multiple tightly coupled VACCs of variable type.},
author = {Williams, Courtney and Chen, Wenyan and Lee, Chia and Yaeger, Daniel and Vyleta, Nicholas and Smith, Stephen},
journal = {Nature Neuroscience},
number = {9},
pages = {1195 -- 1197},
publisher = {Nature Publishing Group},
title = {{Coactivation of multiple tightly coupled calcium channels triggers spontaneous release of GABA}},
doi = {10.1038/nn.3162},
volume = {15},
year = {2012},
}
@article{3122,
abstract = {Since Darwin's pioneering research on plant reproductive biology (e.g. Darwin 1877), understanding the mechanisms maintaining the diverse sexual strategies of plants has remained an important challenge for evolutionary biologists. In some species, populations are sexually polymorphic and contain two or more mating morphs (sex phenotypes). Differences in morphology or phenology among the morphs influence patterns of non-random mating. In these populations, negative frequency-dependent selection arising from disassortative (intermorph) mating is usually required for the evolutionary maintenance of sexual polymorphism, but few studies have demonstrated the required patterns of non-random mating. In the current issue of Molecular Ecology, Shang (2012) make an important contribution to our understanding of how disassortative mating influences sex phenotype ratios in Acer pictum subsp. mono (painted maple), a heterodichogamous, deciduous tree of eastern China. They monitored sex expression in 97 adults and used paternity analysis of open-pollinated seed to examine disassortative mating among three sex phenotypes. Using a deterministic 'pollen transfer' model, Shang et al. present convincing evidence that differences in the degree of disassortative mating in progeny arrays of the sex phenotypes can explain their uneven frequencies in the adult population. This study provides a useful example of how the deployment of genetic markers, demographic monitoring and modelling can be integrated to investigate the maintenance of sexual diversity in plants. },
author = {Field, David and Barrett, Spencer},
journal = {Molecular Ecology},
number = {15},
pages = {3640 -- 3643},
publisher = {Wiley-Blackwell},
title = {{Disassortative mating and the maintenance of sexual polymorphism in painted maple}},
doi = {10.1111/j.1365-294X.2012.05643.x},
volume = {21},
year = {2012},
}
@inproceedings{3123,
abstract = {We introduce the idea of using an explicit triangle mesh to track the air/fluid interface in a smoothed particle hydrodynamics (SPH) simulator. Once an initial surface mesh is created, this mesh is carried forward in time using nearby particle velocities to advect the mesh vertices. The mesh connectivity remains mostly unchanged across time-steps; it is only modified locally for topology change events or for the improvement of triangle quality. In order to ensure that the surface mesh does not diverge from the underlying particle simulation, we periodically project the mesh surface onto an implicit surface defined by the physics simulation. The mesh surface gives us several advantages over previous SPH surface tracking techniques. We demonstrate a new method for surface tension calculations that clearly outperforms the state of the art in SPH surface tension for computer graphics. We also demonstrate a method for tracking detailed surface information (like colors) that is less susceptible to numerical diffusion than competing techniques. Finally, our temporally-coherent surface mesh allows us to simulate high-resolution surface wave dynamics without being limited by the particle resolution of the SPH simulation.},
author = {Yu, Jihun and Wojtan, Christopher J and Turk, Greg and Yap, Chee},
booktitle = {Computer Graphics Forum},
location = {Cagliari, Sardinia, Italy},
number = {2},
pages = {815 -- 824},
publisher = {Blackwell Publishing},
title = {{Explicit mesh surfaces for particle based fluids}},
doi = {10.1111/j.1467-8659.2012.03062.x},
volume = {31},
year = {2012},
}
@inproceedings{3124,
abstract = {We consider the problem of inference in a graphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pairwise terms over a discretized domain. This allows the use of techniques originally developed for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can outperform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions.
},
author = {Korc, Filip and Kolmogorov, Vladimir and Lampert, Christoph},
location = {Edinburgh, Scotland},
publisher = {ICML},
title = {{Approximating marginals using discrete energy minimization}},
year = {2012},
}
@inproceedings{3125,
abstract = {We propose a new learning method to infer a mid-level feature representation that combines the advantage of semantic attribute representations with the higher expressive power of non-semantic features. The idea lies in augmenting an existing attribute-based representation with additional dimensions for which an autoencoder model is coupled with a large-margin principle. This construction allows a smooth transition between the zero-shot regime with no training example, the unsupervised regime with training examples but without class labels, and the supervised regime with training examples and with class labels. The resulting optimization problem can be solved efficiently, because several of the necessity steps have closed-form solutions. Through extensive experiments we show that the augmented representation achieves better results in terms of object categorization accuracy than the semantic representation alone.},
author = {Sharmanska, Viktoriia and Quadrianto, Novi and Lampert, Christoph},
location = {Florence, Italy},
number = {PART 5},
pages = {242 -- 255},
publisher = {Springer},
title = {{Augmented attribute representations}},
doi = {10.1007/978-3-642-33715-4_18},
volume = {7576},
year = {2012},
}
@inproceedings{3126,
abstract = {In this work we propose a new information-theoretic clustering algorithm that infers cluster memberships by direct optimization of a non-parametric mutual information estimate between data distribution and cluster assignment. Although the optimization objective has a solid theoretical foundation it is hard to optimize. We propose an approximate optimization formulation that leads to an efficient algorithm with low runtime complexity. The algorithm has a single free parameter, the number of clusters to find. We demonstrate superior performance on several synthetic and real datasets.
},
author = {Müller, Andreas and Nowozin, Sebastian and Lampert, Christoph},
location = {Graz, Austria},
pages = {205 -- 215},
publisher = {Springer},
title = {{Information theoretic clustering using minimal spanning trees}},
doi = {10.1007/978-3-642-32717-9_21},
volume = {7476},
year = {2012},
}