Single-exponential algorithm for simple grammar bisimilarity yields first polynomial-time equivalence check for context-free session types via linear-valuation conversion.
A Short Decidability Proof for DPDA Language Equivalence via First-Order Grammars
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
The main aim of the paper is to give a short self-contained proof of the decidability of language equivalence for deterministic pushdown automata, which is the famous problem solved by G. Senizergues, for which C. Stirling has derived a primitive recursive complexity upper bound. The proof here is given in the framework of first-order grammars, which seems to be particularly apt for the aim. An appendix presents a modification of Stirling's approach, yielding a complexity bound of the form tetr(2,g(n)) where tetr is the (nonelementary) operator of iterated exponentiation (tetration) and g is an elementary function of the input size.
fields
cs.FL 1years
2024 1verdicts
UNVERDICTED 1representative citing papers
citing papers explorer
-
Simple grammar bisimilarity, with an application to session type equivalence
Single-exponential algorithm for simple grammar bisimilarity yields first polynomial-time equivalence check for context-free session types via linear-valuation conversion.