Modal logic allows to formalize in a very natural way reasoning about a world that dynamically changes under effects of actions, by representing actions by means of modal operators. In this context, we have developed, in collaboration with Camilla Schwind of Marseille, a modal action theory in which persistency is achieved by using a nonmonotonic formalism which maximizes persistency assumptions [23]. The problem of ramification is tackled by introducing a modal causality operator which is used to represent causal rules. Furthermore, we have studied the clausal fragment of this action theory by defining a modal logic programming language to reason about actions [6]. The language can be regarded as an extension of Gelfond and Lifschitz' high-level action language A.
More recently, we have defined a further extension of this language called DyLOG, which allows to define procedures, to build up complex actions from elementary ones [7]. Moreover, it allows to specify action preconditions making use of existential modal operators. A goal-directed proof procedure for the language is provided. The frame problem is given a non-monotonic solution in the context of an abductive characterization.