Completed Hennessy-Milner logic. Remains to implement parser of HML.