TY - GEN AB - We introduce TopoCut: a new way to integrate knowledge about topological properties (TPs) into random field image segmentation model. Instead of including TPs as additional constraints during minimization of the energy function, we devise an efficient algorithm for modifying the unary potentials such that the resulting segmentation is guaranteed with the desired properties. Our method is more flexible in the sense that it handles more topology constraints than previous methods, which were only able to enforce pairwise or global connectivity. In particular, our method is very fast, making it for the first time possible to enforce global topological properties in practical image segmentation tasks. AU - Chen, Chao AU - Freedman, Daniel AU - Lampert, Christoph ID - 5386 SN - 2664-1690 TI - Enforcing topological constraints in random field image segmentation ER - TY - GEN AB - We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures. AU - Wies, Thomas AU - Muñiz, Marco AU - Kuncak, Viktor ID - 5383 SN - 2664-1690 TI - On an efficient decision procedure for imperative tree data structures ER - TY - GEN AB - 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 for every ε > 0 there is a word that is accepted with probability at least 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 words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. AU - Chatterjee, Krishnendu AU - Tracol, Mathieu ID - 5384 SN - 2664-1690 TI - Decidable problems for probabilistic automata on infinite words ER - TY - CONF AB - We introduce TopoCut: a new way to integrate knowledge about topological properties (TPs) into random field image segmentation model. Instead of including TPs as additional constraints during minimization of the energy function, we devise an efficient algorithm for modifying the unary potentials such that the resulting segmentation is guaranteed with the desired properties. Our method is more flexible in the sense that it handles more topology constraints than previous methods, which were only able to enforce pairwise or global connectivity. In particular, our method is very fast, making it for the first time possible to enforce global topological properties in practical image segmentation tasks. AU - Chen, Chao AU - Freedman, Daniel AU - Lampert, Christoph ID - 3336 SN - 978-1-4577-0394-2 T2 - CVPR: Computer Vision and Pattern Recognition TI - Enforcing topological constraints in random field image segmentation ER - TY - CONF AB - We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures. AU - Wies, Thomas AU - Muñiz, Marco AU - Kuncak, Viktor ID - 3323 TI - An efficient decision procedure for imperative tree data structures VL - 6803 ER -