Strong Forgetting in Hennessy-Milner Logic
摘要
This paper concerns the problem of how to revise reactive systems for new specification in inertial principle. It proposes a notion of the weakest sufficient condition (WSC) for Hennessy-Milner logic and sets up a close connection with knowledge forgetting by generalizing the notion of strong bisimulation to restricted actions in Milner’s calculus of communicating system. In principle, it suffices to revise a given system to meet the WSC of new specification.