Document Open Access Logo

Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors Pablo Barceló , Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin , Reino Niskanen

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.103.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

Pablo Barceló
  • Department of Computer Science, University of Chile, Santiago, Chile
  • IMFD, Santiago, Chile
Chih-Duo Hong
  • Department of Computer Science, University of Oxford, UK
Xuan-Bach Le
  • Department of Computer Science, University of Oxford, UK
Anthony W. Lin
  • Technische Universität Kaiserslautern, Germany
Reino Niskanen
  • Department of Computer Science, University of Oxford, UK

Funding

Barceló is funded by the Millennium Institute for Foundational Research on Data (IMFD) and Fondecyt grant 1170109. Le, Lin, and Niskanen are supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement no 759969).

Acknowledgements

We thank Leonid Libkin for the useful discussion.

Cite AsGet BibTex

Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen. Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 103:1-103:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ICALP.2019.103

Abstract

Monadic decomposibility - the ability to determine whether a formula in a given logical theory can be decomposed into a boolean combination of monadic formulas - is a powerful tool for devising a decision procedure for a given logical theory. In this paper, we revisit a classical decision problem in automata theory: given a regular (a.k.a. synchronized rational) relation, determine whether it is recognizable, i.e., it has a monadic decomposition (that is, a representation as a boolean combination of cartesian products of regular languages). Regular relations are expressive formalisms which, using an appropriate string encoding, can capture relations definable in Presburger Arithmetic. In fact, their expressive power coincide with relations definable in a universal automatic structure; equivalently, those definable by finite set interpretations in WS1S (Weak Second Order Theory of One Successor). Determining whether a regular relation admits a recognizable relation was known to be decidable (and in exponential time for binary relations), but its precise complexity still hitherto remains open. Our main contribution is to fully settle the complexity of this decision problem by developing new techniques employing infinite Ramsey theory. The complexity for DFA (resp. NFA) representations of regular relations is shown to be NLOGSPACE-complete (resp. PSPACE-complete).

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Theory of computation → Transducers
  • Theory of computation → Complexity classes
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Transducers
  • Automata
  • Synchronized Rational Relations
  • Ramsey Theory
  • Variable Independence
  • Automatic Structures

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: a framework for efficient analysis of string constraints. In Proceedings of PLDI 2017, pages 602-617. ACM, 2017. URL: http://dx.doi.org/10.1145/3062341.3062384.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer. TRAU: SMT solver for string constraints. In Formal Methods in Computer Aided Design, FMCAD 2018, 2018. Google Scholar
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String Constraints for Verification. In Proceedings of CAV 2014, volume 8559 of LNCS, pages 150-166. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08867-9_10.
  4. James Bailey, Guozhu Dong, and Anthony Widjaja To. Logical queries over views: Decidability and expressiveness. ACM Trans. Comput. Log., 11(2):8:1-8:35, 2010. URL: http://dx.doi.org/10.1145/1656242.1656243.
  5. Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen. Monadic Decomposability of Regular Relations. CoRR, abs/1903.00728, 2019. URL: http://arxiv.org/abs/1903.00728.
  6. Michael Benedikt, Leonid Libkin, Thomas Schwentick, and Luc Segoufin. Definable relations and first-order query languages over strings. J. ACM, 50(5):694-751, 2003. URL: http://dx.doi.org/10.1145/876638.876642.
  7. Jean Berstel. Transductions and Context-Free Languages. Teubner-Verlag, 1979. Google Scholar
  8. Achim Blumensath. Automatic Structures. PhD thesis, RWTH Aachen, 1999. Google Scholar
  9. George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, fifth edition, 2007. Google Scholar
  10. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Springer, 1997. Google Scholar
  11. Cristian Cadar and Koushik Sen. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM, 56(2):82-90, 2013. URL: http://dx.doi.org/10.1145/2408776.2408795.
  12. Olivier Carton, Christian Choffrut, and Serge Grigorieff. Decision problems among the main subfamilies of rational relations. RAIRO - Theoretical Informatics and Applications, 40(2):255-275, 2006. URL: http://dx.doi.org/10.1051/ita:2006005.
  13. Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. What is decidable about string constraints with the ReplaceAll function. PACMPL, 2(POPL):3:1-3:29, 2018. URL: http://dx.doi.org/10.1145/3158091.
  14. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. PACMPL, 3(POPL):49:1-49:30, 2019. URL: http://dx.doi.org/10.1145/3290362.
  15. Christian Choffrut. Relations over words and logic: A chronology. Bull. of the EATCS, 89:159-163, 2006. Google Scholar
  16. Thomas Colcombet and Christof Löding. Transforming structures by set interpretations. Logical Methods in Computer Science, 3(2), 2007. URL: http://dx.doi.org/10.2168/LMCS-3(2:4)2007.
  17. Patrick Cousot and Radhia Cousot. Systematic Design of Program Analysis Frameworks. In Proceedings of POPL 1979, pages 269-282, 1979. URL: http://dx.doi.org/10.1145/567752.567778.
  18. Calvin C. Elgot and Jorge E. Mezei. On Relations Defined by Generalized Finite Automata. IBM J. Res. Dev., 9(1):47-68, 1965. URL: http://dx.doi.org/10.1147/rd.91.0047.
  19. Patrick C. Fischer and Arnold L. Rosenberg. Multitape One-Way Nonwriting Automata. J. Comput. Syst. Sci., 2(1):88-101, 1968. URL: http://dx.doi.org/10.1016/S0022-0000(68)80006-6.
  20. Christiane Frougny and Jacques Sakarovitch. Synchronized Rational Relations of Finite and Infinite Words. Theor. Comput. Sci., 108(1):45-82, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90230-Q.
  21. Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. Word Equations with Length Constraints: What’s Decidable? In Proceedings of HVC 2012, pages 209-226. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-39611-3_21.
  22. Bernard R. Hodgson. Decidabilite par automate fini. Ann. Sc. Math. Quebec, 7:39-57, 1983. Google Scholar
  23. Jean-Louis Imbert. Redundancy, Variable Elimination and Linear Disequations. In Proceedings of ILPS 1994, pages 139-153, 1994. Google Scholar
  24. Gabriel Kuper, Leonid Libkin, and Jan Paredaens. Constraint Databases. Springer Publishing Company, Incorporated, first edition, 2010. Google Scholar
  25. Leonid Libkin. Variable Independence, Quantifier Elimination, and Constraint Representations. In Proceedings of ICALP 2000, volume 1853 of LNCS, pages 260-271. Springer, 2000. URL: http://dx.doi.org/10.1007/3-540-45022-X_23.
  26. Anthony W. Lin and Pablo Barceló. String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS. In Proceedings POPL 2016, pages 123-136. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837641.
  27. Christof Löding and Christopher Spinrath. Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words. In Proceedings of FCT 2017, volume 10472 of LNCS, pages 341-354. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-662-55751-8_27.
  28. Christof Löding and Christopher Spinrath. Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words. Discrete Mathematics &Theoretical Computer Science, 21(3), 2019. URL: https://dmtcs.episciences.org/5141.
  29. Albert R. Meyer and Larry J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In 13th Annual Symposium on Switching and Automata Theory (SWAT 1972), pages 125-129. IEEE, 1972. URL: http://dx.doi.org/10.1109/swat.1972.29.
  30. M. Nivat. Transduction des langages de Chomsky. Ann. Inst. Fourier, 18:339-455, 1968. Google Scholar
  31. Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009. Google Scholar
  32. Michael Sipser. Introduction to the Theory of Computation. Thomson Course Technology Boston, second edition, 2006. Google Scholar
  33. Richard Edwin Stearns. A Regularity Test for Pushdown Machines. Information and Control, 11(3):323-340, 1967. URL: http://dx.doi.org/10.1016/S0019-9958(67)90591-8.
  34. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD thesis, LFCS, School of Informatics, University of Edinburgh, 2010. Google Scholar
  35. A. W. To and Leonid Libkin. Recurrent Reachability Analysis in Regular Model Checking. In LPAR, pages 198-213, 2008. URL: http://dx.doi.org/10.1007/978-3-540-89439-1_15.
  36. Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In Proceedings of CCS 2014, pages 1232-1243. ACM, 2014. URL: http://dx.doi.org/10.1145/2660267.2660372.
  37. Leslie G. Valiant. Regularity and Related Problems for Deterministic Pushdown Automata. Journal of the ACM, 22(1):1-10, 1975. URL: http://dx.doi.org/10.1145/321864.321865.
  38. Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, and Sergey Bereg. Monadic Decomposition. Journal of the ACM, 64(2):1-28, 2017. URL: http://dx.doi.org/10.1145/3040488.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact