A proof of decidability of equivalence between deterministic pushdown autom
ata is presented using a mixture of methods developed in concurrency and la
nguage theory. The technique appeals to a tableau proof system for equivale
nce of configurations of strict deterministic grammars. (C) 2001 Elsevier S
cience B.V. All rights reserved.