Weakest sufficient conditions of HML under weak bisimulation in communicating systems

Ubiquitous reactive systems compute by reacting to stimuli from their environment. Their concurrence, nondeterminism and communication behaviours can usually be captured in the well-known Calculus of Communicating Systems (CCS), among other methods. Reactive systems usually suffer from changes related to fixing bugs or new requirements. This paper concerns the problem of automated revision of reactive systems for new requirements in some principle and observable way: A component should remain unchanged unless modification is necessary from the perspective of external observers. For this purpose, this paper generalizes the weak bisimulation of the CCS to given actions and presents a weak forgetting to logically discard given actions for the observable Hennessy-Milner Logic H^O H O , which can capture the behaviour equivalence of the CCS under weak bisimulation. Finally, the weakest sufficient condition for H^O H O theories is established via weak forgetting. This sufficient condition provides a theoretical foundation for automated revision of reactive systems (CCS) under the desired principle when the new requirements are expressed as H^O H O formulas.