Symbolic solving of extended regular expression inequalities
From MaRDI portal
Abstract: This paper presents a new solution to the containment problem for extended regular expressions that extends basic regular expressions with intersection and complement operators and consider regular expressions on infinite alphabets based on potentially infinite character sets. Standard approaches deciding the containment do not take extended operators or character sets into account. The algorithm avoids the translation to an expression-equivalent automaton and provides a purely symbolic term rewriting systems for solving regular expressions inequalities. We give a new symbolic decision procedure for the containment problem based on Brzozowski's regular expression derivatives and Antimirov's rewriting approach to check containment. We generalize Brzozowski's syntactic derivative operator to two derivative operators that work with respect to (potentially infinite) representable character sets.
Recommendations
Cited in
(9)- The inclusion problem for regular expressions
- A synchronous effects logic for temporal verification of pure Esterel
- scientific article; zbMATH DE number 2043550 (Why is no real title available?)
- Constrained expressions and their derivatives
- Inferring Symbolic Automata
- Automated temporal verification for algebraic effects
- Incremental dead state detection in logarithmic time
- Rewriting extended regular expressions
- An SMT solver for regular expressions and linear arithmetic over string length
This page was built for publication: Symbolic solving of extended regular expression inequalities
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2978511)
