@inproceedings{3341,
abstract = {We consider two-player stochastic games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with \omega-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity gameswith respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition function is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal).},
author = {Chatterjee, Krishnendu},
location = {Tallinn, Estonia},
pages = {270 -- 285},
publisher = {Springer},
title = {{Robustness of structurally equivalent concurrent parity games}},
doi = {10.1007/978-3-642-28729-9_18},
volume = {7213},
year = {2012},
}
@inproceedings{2957,
abstract = {We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether words are accepted with probability arbitrarily close to 1. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound.},
author = {Chatterjee, Krishnendu and Tracol, Mathieu},
booktitle = {Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science},
location = {Dubrovnik, Croatia },
publisher = {IEEE},
title = {{Decidable problems for probabilistic automata on infinite words}},
doi = {10.1109/LICS.2012.29},
year = {2012},
}
@article{3249,
abstract = {Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability". We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun},
journal = {Theoretical Computer Science},
number = {1},
pages = {21 -- 35},
publisher = {Elsevier},
title = {{Simulation distances}},
doi = {10.1016/j.tcs.2011.08.002},
volume = {413},
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},
}
@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},
}
@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},
}
@article{3246,
abstract = {Visualizing and analyzing shape changes at various scales, ranging from single molecules to whole organisms, are essential for understanding complex morphogenetic processes, such as early embryonic development. Embryo morphogenesis relies on the interplay between different tissues, the properties of which are again determined by the interaction between their constituent cells. Cell interactions, on the other hand, are controlled by various molecules, such as signaling and adhesion molecules, which in order to exert their functions need to be spatiotemporally organized within and between the interacting cells. In this review, we will focus on the role of cell adhesion functioning at different scales to organize cell, tissue and embryo morphogenesis. We will specifically ask how the subcellular distribution of adhesion molecules controls the formation of cell-cell contacts, how cell-cell contacts determine tissue shape, and how tissue interactions regulate embryo morphogenesis.},
author = {Barone, Vanessa and Heisenberg, Carl-Philipp J},
journal = {Current Opinion in Cell Biology},
number = {1},
pages = {148 -- 153},
publisher = {Elsevier},
title = {{Cell adhesion in embryo morphogenesis}},
doi = {10.1016/j.ceb.2011.11.006},
volume = {24},
year = {2012},
}
@inproceedings{3264,
abstract = {Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.},
author = {Gupta, Ashutosh and Popeea, Corneliu and Rybalchenko, Andrey},
editor = {Yang, Hongseok},
location = {Kenting, Taiwan},
pages = {188 -- 203},
publisher = {Springer},
title = {{Solving recursion-free Horn clauses over LI+UIF}},
doi = {10.1007/978-3-642-25318-8_16},
volume = {7078},
year = {2011},
}