Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence

TL;DR

This paper proves the decidability of whether a configuration of a pushdown automaton is bisimilar to some finite-state process, extending previous results and solving an open problem for nondeterministic PDA.

Contribution

It introduces a decision procedure for bisimilarity of PDA configurations to finite-state processes using first-order grammars, covering nondeterministic cases previously unresolved.

Findings

Decidability of bisimilarity for nondeterministic PDA established.

Framework based on first-order grammars equivalent to PDA with epsilon-steps.

Extension of regularity problem results for deterministic PDA.

Abstract

The problem if a given configuration of a pushdown automaton (PDA) is bisimilar with some (unspecified) finite-state process is shown to be decidable. The decidability is proven in the framework of first-order grammars, which are given by finite sets of labelled rules that rewrite roots of first-order terms. The framework is equivalent to PDA where also deterministic (i.e. alternative-free) epsilon-steps are allowed, i.e. to the model for which S\'enizergues showed an involved procedure deciding bisimilarity (1998, 2005). Such a procedure is here used as a black-box part of the algorithm. The result extends the decidability of the regularity problem for deterministic PDA that was shown by Stearns (1967), and later improved by Valiant (1975) regarding the complexity. The decidability question for nondeterministic PDA, answered positively here, had been open (as indicated, e.g., by Broadbent and G\"oller, 2012).