Deciding Regularity of the Set of Instances of a Set of Terms with Regular Constraints is EXPTIME-Complete

Omer Giménez, Guillem Godoy, Sebastian Maneth

Research output: Contribution to journalArticlepeer-review

Abstract

Finite-state tree automata are a well-studied formalism for representing term languages. This paper studies the problem of determining the regularity of the set of instances of a finite set of terms with variables, where each variable is restricted to instantiations of a regular set given by a tree automaton. The problem was recently proved decidable, but with an unknown complexity. Here, the exact complexity of the problem is determined by proving EXPTIME-completeness. The main contribution is a new, exponential time algorithm that performs various exponential transformations on the involved terms and tree automata and decides regularity by analyzing formulas over inequation and height predicates.
Original languageEnglish
Pages (from-to)446-464
Number of pages19
JournalSIAM Journal on Computing
Volume40
Issue number2
DOIs
Publication statusPublished - 2011

Fingerprint

Dive into the research topics of 'Deciding Regularity of the Set of Instances of a Set of Terms with Regular Constraints is EXPTIME-Complete'. Together they form a unique fingerprint.

Cite this