Maximal Synthesis for Hennessy-Milner Logic

What is it about?

This paper concerns the maximal synthesis for Hennessy-Milner Logic on Kripke-structures with labeled transitions. We formally define, and prove the validity of, a theoretical framework which modifies a Kripke-model to the least possible extent, in order to satisfy a given HML formula. Applications of this work can be found in the field of controller synthesis and supervisory control for discrete-event systems. Synthesis is realized technically by first projecting the given Kripke-model onto a bisimulation-equivalent partial tree representation, thereby unfolding up to the depth of the synthesized formula. Operational rules then define the required adaptations upon this structure in order to achieve validity of the synthesized formula. Synthesis might result in multiple valid adaptations, which are all related to the original model via simulation. Each simulant of the original Kripke-model, which satisfies the synthesized formula, is also related to one of the synthesis results via simulation. This indicates maximality, or maximal permissiveness, in the context of supervisory control. In addition to the formal construction of synthesis as presented in this paper, we present it in algorithmic form and analyze its computational complexity. Computer-verified proofs for two important theorems in this paper have been created using the Coq proof assistant.

Featured Image