Model construction for implicit specifications in modal logic

In top-down design of reactive systems, implicit specifications of the form C(P₁, ..., P_n) sat F are often encountered, where C(P₁, ..., P_n) is a system containing the (unknown) processes P₁, ..., P_n, and F is a specification. We present a method for constructing the processes P₁, ..., P_n (as labelled transition systems) when C is given as a context of process algebra (such as CCS), and F is given as a formula of Hennessy-Milner Logic extended with maximal recursion. The main contribution is the treatment of the simultaneous construction of several processes which together act as a model for the specification. We have implemented two prototype tools (a semi-automatic as well as an automatic one) which are based on the presented theory.