AbstractIn this paper, we consider a strict generalization of context-free processes, the pushdown processes, which are particularly interesting for three reasons: First, 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 is 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 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.