In this paper, we consider astrict generalization of context-free processes, the pushdown processes, which are particularly interesting for three reasons: First, in contrast to context-free processes that do not support the construction of distributed systems, they are closed under parallel composition with finite state systems. This is shown by proving a new expansion theorem, whose implied 'representation explosion' is no worse than for finite state systems. Second, they are the smallest extension of context-free processes allowing parallel composition with finite state processes, which we prove by showing that every pushdown process ist bisimilar to a (relabelled) parallel composition of a context-free process (namely a stack) with some finite process. Third, they can be model checked by means of an elegant adaptation to pushdown automata of the higher order model checker introduced in [B#92]. As arbitrary parallel composition between context-free processes provides Turing power, and therefore destroys every hope for automatic verification, pushdown process can be considered as the appropriate generalization of context-free processes for frameworks for automatic verification.
cetindag@fmi.uni-passau.de
Ulrike Peiker, Martin Griebl