A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910018053341184 |
|---|---|
| author | Nakamura, Yoshiki |
| author_facet | Nakamura, Yoshiki |
| contents | We consider (logical) reasoning for regular expressions with lookahead (REwLA). In this paper, we give an axiomatic characterization for both the (match-)language equivalence and the largest substitution-closed equivalence that is sound for the (match-)language equivalence. To achieve this, we introduce a variant of propositional dynamic logic (PDL) on finite linear orders, extended with two operators: the restriction to the identity relation and the restriction to its complement. Our main contribution is a sound and complete Hilbert-style finite axiomatization for the logic, which captures the equivalences of REwLA. Using the extended operators, the completeness is established via a reduction into an identity-free variant of PDL on finite strict linear orders. Moreover, the extended PDL has the same computational complexity as REwLA. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_15214 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead Nakamura, Yoshiki Logic in Computer Science Formal Languages and Automata Theory We consider (logical) reasoning for regular expressions with lookahead (REwLA). In this paper, we give an axiomatic characterization for both the (match-)language equivalence and the largest substitution-closed equivalence that is sound for the (match-)language equivalence. To achieve this, we introduce a variant of propositional dynamic logic (PDL) on finite linear orders, extended with two operators: the restriction to the identity relation and the restriction to its complement. Our main contribution is a sound and complete Hilbert-style finite axiomatization for the logic, which captures the equivalences of REwLA. Using the extended operators, the completeness is established via a reduction into an identity-free variant of PDL on finite strict linear orders. Moreover, the extended PDL has the same computational complexity as REwLA. |
| title | A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2601.15214 |