This paper presents a decomposition technique for Hennessy-Milner logic with past and its extension with recursively de??ned formulae. In order to highlight the main ideas and technical tools, processes are described using a subset of CCS with parallel composition, nondeterministic choice, action pre??xing and the inaction constant. The study focuses on developing decompositional reasoning techniques for parallel contexts in that language.
|Name||Computer science reports|