<p>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 <InlineEquation ID="IEq1"> <EquationSource Format="TEX">$\varvec{\mathcal {H}}^{\varvec{O}}$</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mrow> <mi mathvariant="bold-script">H</mi> </mrow> <mrow> <mi mathvariant="bold-italic">O</mi> </mrow> </msup> </math></EquationSource> </InlineEquation>, which can capture the behaviour equivalence of the CCS under weak bisimulation. Finally, the weakest sufficient condition for <InlineEquation ID="IEq2"> <EquationSource Format="TEX">$\varvec{\mathcal {H}}^{\varvec{O}}$</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mrow> <mi mathvariant="bold-script">H</mi> </mrow> <mrow> <mi mathvariant="bold-italic">O</mi> </mrow> </msup> </math></EquationSource> </InlineEquation> 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 <InlineEquation ID="IEq3"> <EquationSource Format="TEX">$\varvec{\mathcal {H}}^{\varvec{O}}$</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mrow> <mi mathvariant="bold-script">H</mi> </mrow> <mrow> <mi mathvariant="bold-italic">O</mi> </mrow> </msup> </math></EquationSource> </InlineEquation> formulas.</p>

Weakest sufficient conditions of HML under weak bisimulation in communicating systems

期刊论文
出版模式：

开放获取
发表日期：

2026年1月24日

查看全文

Xin Zhou,
Yisong Wang,
Renyan Feng,
Jonas Hansen,
Panfeng Chen,
Hongbo Hu,
Songhang Xu

摘要

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 $\varvec{\mathcal {H}}^{\varvec{O}}$ $H^{O}$ , which can capture the behaviour equivalence of the CCS under weak bisimulation. Finally, the weakest sufficient condition for $\varvec{\mathcal {H}}^{\varvec{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 $\varvec{\mathcal {H}}^{\varvec{O}}$ $H^{O}$ formulas.