Advertisement

Monadic Decomposition

  • Margus Veanes
  • Nikolaj Bjørner
  • Lev Nachmanson
  • Sergey Bereg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

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 arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.

Keywords

Disjunctive Normal Form Boolean Combination Presburger Arithmetic Monadic Predicate Automaton Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    URL Encode and Decode Tool, http://www.url-encode-decode.com
  2. 2.
  3. 3.
    Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley (2006)Google Scholar
  4. 4.
    Albarghouthi, A., Gurfinkel, A.: Personal communication (January 2014)Google Scholar
  5. 5.
    Andréka, H., Németi, I., van Benthem, J.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic 27, 217–274 (1998)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Bés, A.: An application of the Feferman-Vaught theorem to automata and logics for words over an infinite alphabet. Logical Methods in Computer Science 4, 1–23 (2008)CrossRefGoogle Scholar
  7. 7.
    Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer (1997)Google Scholar
  8. 8.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), pp. 1–11. Stanford Univ. Press (1962)Google Scholar
  9. 9.
    D’Antoni, L., Veanes, M.: Equivalence of extended symbolic finite transducers. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 624–639. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    D’Antoni, L., Veanes, M.: Static analysis of string encoders and decoders. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 209–228. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  11. 11.
    D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: POPL 2014, pp. 541–553. ACM (2014)Google Scholar
  12. 12.
    De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
  13. 13.
    Feferman, S., Vaught, R.L.: The first-order properties of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959)zbMATHMathSciNetGoogle Scholar
  14. 14.
    Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: SIAMAMS: Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied Mathematics, pp. 27–41 (1974)Google Scholar
  15. 15.
    Ganzinger, H., Meyer, C., Veanes, M.: The two-variable guarded fragment with transitive relations. In: LICS 1999, pp. 24–34. IEEE (1999)Google Scholar
  16. 16.
    Grädel, E.: On the restraining power of guards. Journal of Symbolic Logic 64, 1719–1742 (1998)CrossRefGoogle Scholar
  17. 17.
    Grädel, E.: Why are modal logics so robustly decidable? Bulletin EATCS 68, 90–103 (1999)zbMATHGoogle Scholar
  18. 18.
    Gurevich, Y.: Monadic second-order theories. In: Barwise, J., Feferman, S. (eds.) Model-Theoretical Logics, ch. XIII, pp. 479–506. Springer (1985)Google Scholar
  19. 19.
    Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  20. 20.
    Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: Proceedings of the USENIX Security Symposium (August 2011)Google Scholar
  21. 21.
    Hooimeijer, P., Veanes, M.: An evaluation of automata algorithms for string analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 248–262. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  22. 22.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison Wesley (1979)Google Scholar
  23. 23.
    Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. International Journal of Foundations of Computer Science 13(4), 571–586 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  24. 24.
    Korovin, K.: Instantiation-based automated reasoning: From theory to practice. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 163–166. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  25. 25.
    Korovin, K.: Inst-gen – A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Ganzinger Festschrift. LNCS, vol. 7797, pp. 239–270. Springer, Heidelberg (2013)Google Scholar
  26. 26.
    Korovin, K.: Personal communication (December 2013)Google Scholar
  27. 27.
    Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL 2014, pp. 607–618. ACM (2014)Google Scholar
  28. 28.
    Löb, M.: Decidability of the monadic predicate calculus with unary function symbols. Journal of Symbolic Logic 32, 563 (1967)Google Scholar
  29. 29.
    Löwenheim, L.: Über Möglichkeiten im Relativkalkül. Math. Annalen 76, 447–470 (1915)CrossRefGoogle Scholar
  30. 30.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (2010)Google Scholar
  31. 31.
    Nipkow, T.: Linear quantifier elimination. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 18–33. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  32. 32.
    Nivat, M.: Transductions des langages de Chomsky. Annales de l’institut Fourier 18(1), 339–455 (1968)CrossRefzbMATHMathSciNetGoogle Scholar
  33. 33.
    Noord, G.V., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4, 263–286 (2001)CrossRefzbMATHMathSciNetGoogle Scholar
  34. 34.
    Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: In Comptes Rendus du I congrés de Mathématiciens des Pays Slaves, Warsaw, Poland, pp. 92–101 (1929)Google Scholar
  35. 35.
    Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)zbMATHMathSciNetGoogle Scholar
  36. 36.
    Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, STOC 1978, pp. 320–325. ACM, New York (1978)CrossRefGoogle Scholar
  37. 37.
    Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc. 74, 358–366 (1953)CrossRefzbMATHMathSciNetGoogle Scholar
  38. 38.
    Saxena, P., Molnar, D., Livshits, B.: Scriptgard: Preventing script injection attacks in legacy web applications with automatic sanitization. Technical Report MSR-TR-2010-128, Microsoft Research (August 2010)Google Scholar
  39. 39.
    Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, vol. 3, pp. 389–455. Springer (1996)Google Scholar
  40. 40.
    The Unicode Consortium. The Unicode Standard 6.3, Emoticons, http://unicode.org/charts/PDF/U1F600.pdf
  41. 41.
    Vardi, M.Y.: Why is modal logic so robustly decidable? In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 31, pp. 149–184. American Mathematical Society (1996)Google Scholar
  42. 42.
    Veanes, M., Bjørner, N.: Symbolic automata: The toolkit. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 472–477. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  43. 43.
    Veanes, M., Bjørner, N., de Moura, L.: Symbolic automata constraint solving. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 640–654. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  44. 44.
    Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjørner, N.: Symbolic finite state transducers: Algorithms and applications. In: POPL 2012, pp. 137–150 (2012)Google Scholar
  45. 45.
    Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41–110. Springer (1997)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Margus Veanes
    • 1
  • Nikolaj Bjørner
    • 1
  • Lev Nachmanson
    • 1
  • Sergey Bereg
    • 2
  1. 1.Microsoft ResearchUSA
  2. 2.The University of Texas at DallasUSA

Personalised recommendations