Cyclic communicating processes: hierarchy and verification

We advocate Cyclic Communicating Processes (CCPs) as a viable and tractable model of computation for reactive systems. As the name suggests, the model consists of a network of sequential agents that communicate with each other. The crucial restriction is that the control flow of each agent is cyclic. The communication mechanism consists of the agents performing common actions together. The first extension consists of endowing the control states with finite number of colors which can serve as abstractions of the values of the variables owned by the agents. This leads to a restricted class of colored Petri nets that one could term as colored marked graphs or colored T-systems. This class of CCPs has a natural semantics in terms of finite 1-safe Petri nets. We concentrate on specification and verification issues related to branching temporal logics for CCPs.