eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-07-04
103:1
103:14
10.4230/LIPIcs.ICALP.2019.103
article
Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming)
Barceló, Pablo
1
2
https://orcid.org/0000-0003-2293-2653
Hong, Chih-Duo
3
Le, Xuan-Bach
3
Lin, Anthony W.
4
https://orcid.org/0000-0003-4715-5096
Niskanen, Reino
3
https://orcid.org/0000-0002-2210-1481
Department of Computer Science, University of Chile, Santiago, Chile
IMFD, Santiago, Chile
Department of Computer Science, University of Oxford, UK
Technische Universität Kaiserslautern, Germany
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol132-icalp2019/LIPIcs.ICALP.2019.103/LIPIcs.ICALP.2019.103.pdf
Transducers
Automata
Synchronized Rational Relations
Ramsey Theory
Variable Independence
Automatic Structures