We describe a framework for compositional verification of finite-state
processes. The framework is based on two ideas: a subset of the logic
CTL for which satisfaction is preserved under composition, and a preo
rder on structures which captures the relation between a component and
a system containing the component. Satisfaction of a formula in the l
ogic corresponds to being below a particular structure (a tableau for
the formula) in the preorder. We show how to do assume-guarantee-style
reasoning within this framework. Additionally, we demonstrate efficie
nt methods for model checking in the logic and for checking the preord
er in several special cases. We have implemented a system based on the
se methods, and we use it to give a compositional verification of a CP
U controller.