Implicit Recursive Characteristics of STOP
This work addresses a foundational gap in process algebra theory for researchers in formal methods and concurrency, but it is incremental as it builds on existing CSP notations.
The paper tackles the lack of formal description for the STOP process in Communicating Sequential Processes (CSP) by introducing a 'nil' event to apply the prefix operator consistently, resulting in a unified process algebra model and a simple formal equation for STOP.
The most important notations of Communicating Sequential Process(CSP) are the process and the prefix (event)$\rightarrow$(process) operator. While we can formally apply the $\rightarrow$ operator to define a live process's behavior, the STOP process, which usually resulted from deadlock, starving or livelock, is lack of formal description, defined by most literatures as "doing nothing but halt". In this paper, we argue that the STOP process should not be considered as a black box, it should follow the prefix $\rightarrow$ schema and the same inference rules so that a unified and consistent process algebra model can be established. In order to achieve this goal, we introduce a special event called "nil" that any process can take. This nil event will do nothing meaningful and leave nothing on a process's observable record. With the nil event and its well-defined rules, we can successfully use the $\rightarrow$ operator to formally describe a process's complete behavior in its whole life circle. More interestingly, we can use prefix $\rightarrow$ and nil event to fully describe the STOP process's internal behavior and conclude that the STOP's formal equation can be given as simple as STOP$_{αX} = μ$ X. nil $\rightarrow$ X.