  This work presents three increasingly expressive Dynamic Logics in which the
programs are CCS processes (sCCS-PDL, CCS-PDL and XCCS-PDL). Their goal is to
reason about properties of concurrent programs and systems described using CCS.
In order to accomplish that, CCS's operators and constructions are added to a
basic modal logic in order to create dynamic logics that are suitable for the
description and verification of properties of communicating, concurrent and
non-deterministic programs and systems, in a similar way as PDL is used for the
sequential case. We provide complete axiomatizations for the three logics.
Unlike Peleg's Concurrent PDL with Channels, our logics have a simple Kripke
semantics, complete axiomatizations and the finite model property.
