I. Walukiewicz, “Pushdown Processes: Games and Model Checking”, BRICS, vol. 3, no. 54, Jun. 1996.