Maximal Synthesis for Hennessy-Milner Logic with the Box Modality

This paper presents a novel approach to adapt a behavioral model in order to satisfy a requirement in Hennessy-Milner Logic, including an additional box modality operator, expressing an invariant formula. Control system synthesis, as defined in this way, retains all non-invalidating behavior, and thereby guarantees maximal permissiveness for supervisory control. This research extends earlier work by embracing a broader synthesized logic, enabling synthesis with respect to invariant formulas for non-deterministic behavioral models. All definitions and proofs in this paper have been computer verified using the Coq proof assistant.