Document

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

## File

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

## Acknowledgements

We thank Leonid Libkin for the useful discussion.

## Cite As

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

## 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.
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.
8. Achim Blumensath. Automatic Structures. PhD thesis, RWTH Aachen, 1999.
9. George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, fifth edition, 2007.
10. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Springer, 1997.
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.
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.
23. Jean-Louis Imbert. Redundancy, Variable Elimination and Linear Disequations. In Proceedings of ILPS 1994, pages 139-153, 1994.
24. Gabriel Kuper, Leonid Libkin, and Jan Paredaens. Constraint Databases. Springer Publishing Company, Incorporated, first edition, 2010.
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.
31. Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009.
32. Michael Sipser. Introduction to the Theory of Computation. Thomson Course Technology Boston, second edition, 2006.
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.
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.