TY - GEN
AB - 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.
AU - Chatterjee, Krishnendu
AU - Chaubal, Siddhesh
AU - Kamath, Pritish
ID - 5378
SN - 2664-1690
TI - Faster algorithms for alternating refinement relations
ER -
TY - GEN
AB - 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.
AU - Korc, Filip
AU - Kolmogorov, Vladimir
AU - Lampert, Christoph
ID - 5396
SN - 2664-1690
TI - Approximating marginals using discrete energy minimization
ER -
TY - GEN
AB - 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.
AU - Porsche, Jana
ID - 5398
TI - Actual state of research data @ ISTAustria
ER -
TY - CHAP
AU - Gupta, Ashutosh
ID - 5745
SN - 0302-9743
T2 - Automated Technology for Verification and Analysis
TI - Improved Single Pass Algorithms for Resolution Proof Reduction
VL - 7561
ER -
TY - JOUR
AB - 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.
AU - Pausinger, Florian
ID - 6588
IS - 1
JF - Journal of Mathematical Physics, Analysis, Geometry
SN - 1812-9471
TI - Elementary solutions of the Bernstein problem on two intervals
VL - 8
ER -
TY - CONF
AB - 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.
AU - Beyer, Dirk
AU - Henzinger, Thomas A
AU - Keremoglu, Mehmet
AU - Wendler, Philipp
ID - 1384
T2 - Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering
TI - Conditional model checking: A technique to pass information between verifiers
ER -
TY - JOUR
AB - 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.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
ID - 3846
IS - 2
JF - Journal of Computer and System Sciences
TI - A survey of stochastic ω regular games
VL - 78
ER -
TY - JOUR
AB - 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.
AU - Berberich, Eric
AU - Halperin, Dan
AU - Kerber, Michael
AU - Pogalnikova, Roza
ID - 3115
IS - 4
JF - Discrete & Computational Geometry
TI - Deconstructing approximate offsets
VL - 48
ER -
TY - JOUR
AB - 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.
AU - Kolmogorov, Vladimir
ID - 3117
IS - 15
JF - Discrete Applied Mathematics
TI - Minimizing a sum of submodular functions
VL - 160
ER -
TY - JOUR
AB - 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.
AU - Bojsen-Hansen, Morten
AU - Li, Hao
AU - Wojtan, Christopher J
ID - 3118
IS - 4
JF - ACM Transactions on Graphics
TI - Tracking surfaces with evolving topology
VL - 31
ER -