The modular sequent calculus labelled with truth values for modal systems is revisited. Completeness is obtained over the natural algebraic semantics and over the traditional general Kripke semantics. A duality between the two semantics is established. A simple enrichment of the calculus is shown to be complete over standard Kripke semantics. Rules are given characterizing different properties of the accessibility relation among general frames. Analyticity of the calculus is discussed. This talk reports ongoing joint work with P. Mateus, C. Sernadas and L. Viganò.