Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence.

DOI10.4230/LIPICS.MFCS.2016.52zbMATH Open1398.68367arXiv1305.0516OpenAlexW2542491786MaRDI QIDQ4608615

Publication date: 21 March 2018

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).

Full work available at URL: https://arxiv.org/abs/1305.0516

zbMATH Keywords

regularity bisimulation pushdown processes first-order grammars

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42)