Document Open Access Logo

Symbolic Solving of Extended Regular Expression Inequalities

Authors Matthias Keil, Peter Thiemann

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2014.175.pdf
  • Filesize: 449 kB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Extended regular expression
  • containment
  • infinite alphabet
  • infinite character set
  • effective boolean algebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

This paper presents a new algorithm for the containment problem for extended regular expressions that contain intersection and complement operators and that range over infinite alphabets. The algorithm solves extended regular expressions inequalities symbolically by term rewriting and thus avoids the translation to an expression-equivalent automaton.

Our algorithm is based on Brzozowski's regular expression derivatives and on Antimirov's term-rewriting approach to check containment. To deal with large or infinite alphabets effectively, we generalize Brzozowski's derivative operator to work with respect to (potentially infinite) representable character sets.

Cite As Get BibTex

Matthias Keil and Peter Thiemann. Symbolic Solving of Extended Regular Expression Inequalities. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 175-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.175

Author Details

Matthias Keil
Peter Thiemann

References

  1. Valentin M. Antimirov. Rewriting regular inequalities. In Horst Reichel, editor, FCT, volume 965 of LNCS, pages 116-125. Springer, 1995. Google Scholar
  2. Valentin M. Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theoretical Computer Science, 155(2):291-319, 1996. Google Scholar
  3. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Roberto Giacobazzi and Radhia Cousot, editors, POPL, pages 457-468, Rome, Italy, January 2013. ACM. Google Scholar
  4. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. Google Scholar
  5. Pascal Caron, Jean-Marc Champarnaud, and Ludovic Mignot. Partial derivatives of an extended regular expression. In Adrian Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, LATA, volume 6638 of LNCS, pages 179-191. Springer, 2011. Google Scholar
  6. A. Ginzburg. A procedure for checking equality of regular expressions. J. ACM, 14(2):355-362, April 1967. Google Scholar
  7. Victor M. Glushkov. The abstract theory of automata. Russian Mathematical Surveys, 16(5):1-53, 1961. Google Scholar
  8. Phillip Heidegger, Annette Bieniusa, and Peter Thiemann. Access permission contracts for scripting languages. In John Field and Michael Hicks, editors, Proc. 39th ACM Symp. POPL, pages 111-122, Philadelphia, USA, January 2012. ACM Press. Google Scholar
  9. John Edward Hopcroft and Richard Manning Karp. A linear algorithm for testing equivalence of finite automata. Technical report, Cornell University, 1971. Google Scholar
  10. Harry B. Hunt III, Daniel J. Rosenkrantz, and Thomas G. Szymanski. On the equivalence, containment, and covering problems for the regular and context-free languages. J. Comput. Syst. Sci., 12(2):222-268, 1976. Google Scholar
  11. Tao Jiang and Bala Ravikumar. Minimal NFA problems are hard. SIAM J. Comput., 22(6):1117-1141, 1993. Google Scholar
  12. Matthias Keil and Peter Thiemann. Efficient dynamic access analysis using JavaScript proxies. In Proceedings of the 9th Symposium on Dynamic Languages, DLS'13, pages 49-60, New York, NY, USA, 2013. ACM. Google Scholar
  13. Matthias Keil and Peter Thiemann. Symbolic solving of regular expression inequalities. Technical report, Institute for Computer Science, University of Freiburg, 2014. Google Scholar
  14. Robert McNaughton and Hisao Yamada. Regular expressions and state graphs for automata. Electronic Computers, IRE Transactions on, EC-9(1):39-47, 1960. Google Scholar
  15. Albert R. Meyer and Larry J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In SWAT (FOCS), pages 125-129. IEEE Computer Society, 1972. Google Scholar
  16. Scott Owens, John H. Reppy, and Aaron Turon. Regular-expression derivatives re-examined. J. Funct. Program., 19(2):173-190, 2009. Google Scholar
  17. Valentin N. Redko. On defining relations for the algebra of regular events. Ukrain. Mat., 16:120-126, 1964. Google Scholar
  18. Ken Thompson. Regular expression search algorithm. Commun. ACM, 11(6):419-422, 1968. Google Scholar
  19. Gertjan van Noord and Dale Gerdemann. Finite state transducers with predicates and identities. Grammars, 4(3):263-286, 2001. Google Scholar
  20. Margus Veanes. Applications of symbolic finite automata. In Stavros Konstantinidis, editor, CIAA, volume 7982 of Lecture Notes in Computer Science, pages 16-23, Halifax, NS, Canada, 2013. Springer. Google Scholar
  21. Bruce W. Watson. Implementing and using finite automata toolkits. Nat. Lang. Eng., 2(4):295-302, December 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact