Nordic Journal of Computing Bibliography

O. Burkart and B. Steffen. Composition, decomposition and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89-125, Summer 1995.
Abstract

In 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

Selected references


Shortcuts:

  • Nordic Journal of Computing homepage
  • Bibliography top level
  • Nordic Journal of Computing Author Index
  • Search the HBP database