Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead

Yoshiki Nakamura

TL;DR

The paper develops a complete, finite Hilbert-style axiomatization for a Propositional Dynamic Logic variant over finite linear orders that captures the logic of regular expressions with lookahead (REwLA). By introducing REwLA+ with identities-restriction operators, the authors decompose relational semantics into identity and non-identity components and reduce completeness to an identity-free PDL (PDL^−) on finite strict linear orders. They prove soundness and completeness for REwLA+ and establish matching complexity results: EXPTIME-completeness for substitution-closed equivalences and PSPACE-completeness for standard equivalences. The work also provides an embedding framework linking substitution-closed and standard equivalences to PDL theories, and outlines potential directions for direct equational axiomatizations and extensions to lookbehind or backreferences. Overall, the approach unifies regex reasoning with PDL techniques, delivering a robust semantic and axiomatic foundation for REwLA+ with tractable complexity profiles $($EXPTIME$)$ and $($PSPACE$)$ on appropriate finite-order models.

Abstract

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.

A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead

TL;DR

The paper develops a complete, finite Hilbert-style axiomatization for a Propositional Dynamic Logic variant over finite linear orders that captures the logic of regular expressions with lookahead (REwLA). By introducing REwLA+ with identities-restriction operators, the authors decompose relational semantics into identity and non-identity components and reduce completeness to an identity-free PDL (PDL^−) on finite strict linear orders. They prove soundness and completeness for REwLA+ and establish matching complexity results: EXPTIME-completeness for substitution-closed equivalences and PSPACE-completeness for standard equivalences. The work also provides an embedding framework linking substitution-closed and standard equivalences to PDL theories, and outlines potential directions for direct equational axiomatizations and extensions to lookbehind or backreferences. Overall, the approach unifies regex reasoning with PDL techniques, delivering a robust semantic and axiomatic foundation for REwLA+ with tractable complexity profiles EXPTIME and PSPACE on appropriate finite-order models.

Abstract

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.
Paper Structure (11 sections, 10 theorems, 29 equations, 3 figures)

This paper contains 11 sections, 10 theorems, 29 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. REwLA: Regular Expressions with LookAhead
  4. Relational Semantics, Match-Languages, and Languages
  5. Substitution-Closed Equivalences
  6. PDL
  7. PDL for REwLA+
  8. Embedding equivalences
  9. Soundness and completeness
  10. Identity-Free PDL on Finite Strict Linear Orders
  11. Reduction from the Completeness of Identity-Free PDL

Key Result

proposition thmcounterproposition

]$\wlang( t ) = \wlang( s )$ "iff" $\GRELstfinlin{} \modelsfml t \termendmarker = s \termendmarker$, where $\reintro*\termendmarker \coloneq \left(\sum_{ a \in \exprvsig( t \, s )} a \right)^{\mathtt{\mathop{a}}}$.

Figures (3)

  • Figure 1: Inclusions among the four language equivalences. Each arrow from $X$ to $Y$ means that the equivalence induced by $X$ is a subset of that induced by $Y$.
  • Figure 2: $\HilbertstylePDLREwLAp$: Rules and axioms for $\mathrm{PDL}_{\mathrm{{REwLA+}}}$ on finite linear orders.
  • Figure 3: $\HilbertstyleifreePDLsfinlin$: Rules and axioms for $\mathrm{PDL}^{-}$ on finite strict linear orders.

Theorems & Definitions (14)

  • proposition thmcounterproposition
  • proposition thmcounterproposition
  • proposition thmcounterproposition
  • proposition thmcounterproposition
  • proposition thmcounterproposition
  • theorem 1.1: Main theorem
  • theorem 1.2: \ref{['section: PDL- completeness']}
  • definition thmcounterdefinition
  • proposition thmcounterproposition
  • proof
  • ...and 4 more