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.
Chapter PDF
References
URL Encode and Decode Tool, http://www.url-encode-decode.com
Z3 Python, http://rise4fun.com/Z3Py
Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley (2006)
Albarghouthi, A., Gurfinkel, A.: Personal communication (January 2014)
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)
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)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer (1997)
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)
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)
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)
D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: POPL 2014, pp. 541–553. ACM (2014)
De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
Feferman, S., Vaught, R.L.: The first-order properties of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959)
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)
Ganzinger, H., Meyer, C., Veanes, M.: The two-variable guarded fragment with transitive relations. In: LICS 1999, pp. 24–34. IEEE (1999)
Grädel, E.: On the restraining power of guards. Journal of Symbolic Logic 64, 1719–1742 (1998)
Grädel, E.: Why are modal logics so robustly decidable? Bulletin EATCS 68, 90–103 (1999)
Gurevich, Y.: Monadic second-order theories. In: Barwise, J., Feferman, S. (eds.) Model-Theoretical Logics, ch. XIII, pp. 479–506. Springer (1985)
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)
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)
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)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison Wesley (1979)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. International Journal of Foundations of Computer Science 13(4), 571–586 (2002)
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)
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)
Korovin, K.: Personal communication (December 2013)
Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL 2014, pp. 607–618. ACM (2014)
Löb, M.: Decidability of the monadic predicate calculus with unary function symbols. Journal of Symbolic Logic 32, 563 (1967)
Löwenheim, L.: Über Möglichkeiten im Relativkalkül. Math. Annalen 76, 447–470 (1915)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (2010)
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)
Nivat, M.: Transductions des langages de Chomsky. Annales de l’institut Fourier 18(1), 339–455 (1968)
Noord, G.V., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4, 263–286 (2001)
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)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
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)
Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc. 74, 358–366 (1953)
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)
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, vol. 3, pp. 389–455. Springer (1996)
The Unicode Consortium. The Unicode Standard 6.3, Emoticons, http://unicode.org/charts/PDF/U1F600.pdf
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)
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)
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)
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)
Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41–110. Springer (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Veanes, M., Bjørner, N., Nachmanson, L., Bereg, S. (2014). Monadic Decomposition. In: Biere, A., Bloem, R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham. https://doi.org/10.1007/978-3-319-08867-9_42
Download citation
DOI: https://doi.org/10.1007/978-3-319-08867-9_42
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08866-2
Online ISBN: 978-3-319-08867-9
eBook Packages: Computer ScienceComputer Science (R0)