Monadic Decomposition
Authors: Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg
Paper Information
| Title: | Monadic Decomposition |
| Authors: | Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg |
| Proceedings: | CAV 2014 LNCS Proceedings |
| Editors: | Armin Biere, Swen Jacobs and Roderick Bloem |
| Keywords: | symbolic automata, symbolic transducers, SMT |
| Abstract: | ABSTRACT. Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier free formulas over a decidable background theory, such as linear arithmetic, and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists. |
| Pages: | 18 |
| Talk: | Jul 22 10:45 |
| Paper: |  |