 The translation of formulas and programs into many-sorted logic is the expected  one:[26]  we express in the target logic \(\MSL^{\PDL}\) the semantical interpretation of the formulas and programs being translated.