Title :
Cyclic communicating processes: hierarchy and verification
Author :
Thiagarajan, P.S.
Author_Institution :
Sch. of Comput., Nat. Univ. of Singapore, Singapore
Abstract :
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.
Keywords :
Petri nets; graph colouring; software agents; temporal logic; CCP specification; CCP verification; colored Petri nets; cyclic communicating processes; reactive systems; sequential agents; temporal logic; Application software; Communication system control; Logic; Manipulator dynamics; Petri nets; Processor scheduling; Programming; Reachability analysis; Timing; Yarn;
Conference_Titel :
Application of Concurrency to System Design, 2003. Proceedings. Third International Conference on
Print_ISBN :
0-7695-1887-7
DOI :
10.1109/CSD.2003.1207693