Satisfiability of Context-free String Constraints with Subword-ordering and Transducers
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866929210396770304 |
|---|---|
| author | Aiswarya, C Mal, Soumodev Saivasan, Prakash |
| author_facet | Aiswarya, C Mal, Soumodev Saivasan, Prakash |
| contents | We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NExptime-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size $O(n)$) and $n$ finite-state automata (each of size $O(n)$) can be double exponential in $n$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_07996 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Satisfiability of Context-free String Constraints with Subword-ordering and Transducers Aiswarya, C Mal, Soumodev Saivasan, Prakash Formal Languages and Automata Theory Logic in Computer Science F.1.1; F.3.1; F.4.1 We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NExptime-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size $O(n)$) and $n$ finite-state automata (each of size $O(n)$) can be double exponential in $n$. |
| title | Satisfiability of Context-free String Constraints with Subword-ordering and Transducers |
| topic | Formal Languages and Automata Theory Logic in Computer Science F.1.1; F.3.1; F.4.1 |
| url | https://arxiv.org/abs/2401.07996 |