Abstract:
A proof of decidability of equivalence between deterministic pushdown automata is presented using a mixture of methods developed in concurrency and language theory. The technique appeals to a tableau proof system for equivalence of configurations of strict deterministic grammars.
ECS-LFCS-99-411.
This report is available in the following formats: