AbstractIn this paper, we consider a strict generalization of context-free processes, the

pushdown processes, which are particularly interesting for three reasons: First, they areclosed under parallel compositionwith 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 thesmallestextension of context-free processes allowing parallel composition with finite state processes, which we prove by showing that every pushdown process is bisimilar to a (relabelled) parallel composition of a context-free process (namely a stack) with some finite process. Third, they can bemodel checkedby means of an elegant adaptation to pushdown automata of the second order model checker known for context-free processes. As arbitrary parallel composition between context-free processes provides Turing power, and therefore destroys every hope for automatic verification, pushdown processes can be considered as the appropriate generalization of context-free processes for frameworks for automatic verification.

Categories and Subject Descriptors: F.1.1 [Computation by Abstract Devices]: Models of Computation; F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.4.2 [Mathematical Logic and Formal Languages]: Grammars and Other Rewriting Systems

Additional Key Words and Phrases: infinite-state systems, context-free processes, pushdown processes, parallel composition, model-checking

Selected papers that cite this one

- Colin Stirling. Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 195(2):113-131, 30 March 1998.

Selected references

- Edmund M. Clarke Jr., E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986.

- Rance Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27(8):725-747, 1989.

- E. Allen Emerson and Chin-Laung Lei. Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In Proceedings, Symposium on Logic in Computer Science, pages 267-278, Cambridge, Massachusetts, 16-18 June 1986. IEEE Computer Society.