HP Labs Technical Reports
Click here for full text:
A Finite Branching Result for CCS
Abstract: This paper proves a finite branching property for computations in Milner's Calculus of Communicating Systems (CCS); a closed bounded CCS expression which does not involve relabelling or restriction can only evolve to finitely many expressions for which the amount of parallelism at the top level is less than a given bound. This result is then used to give a description of certain types of observational bisimulations on CCS in terms of a finitary modal logic.
Back to Index