Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words

TL;DR

This paper investigates the decidability and complexity of equivalence and recognizability problems for rational relations over finite and infinite words, revealing undecidability in some cases and providing efficient algorithms in others.

Contribution

It establishes undecidability of the equivalence problem for binary deterministic rational relations over infinite words and improves decision procedures for finite words using polynomial-time tests.

Findings

Equivalence problem for binary deterministic rational relations over infinite words is undecidable.

Decidability of recognizability for automatic relations over infinite words is in doubly exponential time.

Decision procedure for finite words has been improved to single exponential time.

Abstract

We consider decision problems for relations over finite and infinite words defined by finite automata. We prove that the equivalence problem for binary deterministic rational relations over infinite words is undecidable in contrast to the case of finite words, where the problem is decidable. Furthermore, we show that it is decidable in doubly exponential time for an automatic relation over infinite words whether it is a recognizable relation. We also revisit this problem in the context of finite words and improve the complexity of the decision procedure to single exponential time. The procedure is based on a polynomial time regularity test for deterministic visibly pushdown automata, which is a result of independent interest.