Monadic decomposabily of regular relations
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...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
2019
|
| _version_ | 1826305531231338496 |
|---|---|
| author | Barceló, P Hong, C-D Le, XB Lin, A Niskanen, R |
| author_facet | Barceló, P Hong, C-D Le, XB Lin, A Niskanen, R |
| author_sort | Barceló, P |
| collection | OXFORD |
| description | 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). |
| first_indexed | 2024-03-07T06:34:15Z |
| format | Conference item |
| id | oxford-uuid:f70ed1d2-971f-490a-b49d-3d49d6177183 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:34:15Z |
| publishDate | 2019 |
| publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| record_format | dspace |
| spelling | oxford-uuid:f70ed1d2-971f-490a-b49d-3d49d61771832022-03-27T12:39:50ZMonadic decomposabily of regular relationsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f70ed1d2-971f-490a-b49d-3d49d6177183Symplectic Elements at OxfordSchloss Dagstuhl - Leibniz-Zentrum für Informatik2019Barceló, PHong, C-DLe, XBLin, ANiskanen, RMonadic 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). |
| spellingShingle | Barceló, P Hong, C-D Le, XB Lin, A Niskanen, R Monadic decomposabily of regular relations |
| title | Monadic decomposabily of regular relations |
| title_full | Monadic decomposabily of regular relations |
| title_fullStr | Monadic decomposabily of regular relations |
| title_full_unstemmed | Monadic decomposabily of regular relations |
| title_short | Monadic decomposabily of regular relations |
| title_sort | monadic decomposabily of regular relations |
| work_keys_str_mv | AT barcelop monadicdecomposabilyofregularrelations AT hongcd monadicdecomposabilyofregularrelations AT lexb monadicdecomposabilyofregularrelations AT lina monadicdecomposabilyofregularrelations AT niskanenr monadicdecomposabilyofregularrelations |