Separability and decidability results for varieties of Jonsson dynamic algebras

Dynamic algebras are algebraic counterparts of dynamic logics: propositional logical systems endowed with a set of modal operators. In [18], B. Jonsson introduced dynamic algebras as Boolean algebras with unary operators, the indices of which range over a given Kleene algebra. On the other hand, V. R. Pratt and D, Kozen proposed a two-sorted approach to dynamic algebras, which was followed in the early papers on the topic, such as Fischer and Ladner [15] and Nemeti [28]. For a recent overview of the field cf. [4]. In the present paper we investigate connections (as well as diversities) between these two approaches. Our main aim is to transfer (where possible) two-sorted results on separability and decidability to the one-sorted case and to extend them to broad classes of varieties of Jonsson dynamic algebras. In particular, as a consequence of such considerations, we obtain a decidability result on Kleene algebras.