Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Regular Expressions with Dynamic Name Binding

Regular Expressions with Dynamic Name Binding

File(s)
bars.pdf (512.89 KB)
Main article
Permanent Link(s)
https://hdl.handle.net/1813/41188
Collections
Computing and Information Science Technical Reports
Author
Kozen, Dexter
Milius, Stefan
Schröder, Lutz
Wißmann, Thorsten
Abstract

Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language model. Moreover, it has been shown that NKA expressions can be translated into a species of nondeterministic nominal automata, thus providing one half of a Kleene theorem. The other half is known to fail, i.e. there are nominal languages that can be accepted by a nominal automaton but are not definable in NKA. In the present work, we introduce a calculus of regular expressions with dynamic name binding. It satisfies the full Kleene theorem, i.e. it is equivalent to a natural species of nominal automata, and thus strictly more expressive than NKA. We show that containment checking in our calculus is decidable in EXPSPACE, and in fact has polynomial fixed-parameter space complexity. The known EXPSPACE bound for containment of NKA expressions follows.

Description
Content file updated at author's request on 2016-03-03.
Date Issued
2015-10-18
Keywords
Kleene algebra, nominal automata
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance