Representing CCS programs by finite predicate-transition nets (Q1122360)

A construction is given which for every CCS program (in which every choice and recursion starts sequentially) yields a finite and strict predicate/transition net. The main idea is to put the dynamically growing information about action manipulation (i.e. renaming, hiding, restriction) and parallel synchronization into the tokens of the net. All other information is static and can be encoded in the structure of the net. Consistency of this construction is proved not only with respect to the standard interleaving semantics but with respect to the distributed semantics of Degano, De Nicola and Montanari which additionally models the concurrency explicitly.