Pushdown Processes: Parallel Composition and Model Checking

O. Burkart, B. Steffen

	   In this paper we consider a strict generalization of
	   context-free processes, the {\em pushdown processes}, and
	   show that this class of processes is 1) closed under parallel
	   composition with finite state systems, and can 2) be model
	   checked by means of an elegant adaptation of the higher
	   order model checker introduced in [BuS92].  This shows the
	   advantages of pushdown processes over context-free processes,
	   which are not sufficiently general in order to support parallel
	   composition.  [BuS92]: O.Burkart and B.Steffen. Model Checking
	   for Context-Free Processes. In CONCUR '92, LNCS 630, pages
	   123--137. Springer, 1992.