In dealing with transition systems, it is natural to look for logics having the following desirable properties: (1) invariance under (strong) bisimulation (i.e. truth of formulas is preserved by strong bisimulation); (2) decidability.

Standard modal logic and some of its important extensions (logic with star-diamonds for the transitive closure of the transition relation, dynamic modal logic, standard temporal logic with only forward modalities, mu-calculus) have these two properties. Until recently, mu-calculus was the strongest "naturally-defined" logic that I knew having these properties. In fact, mu-calculus can even be seen to be "maximal" in some sense with respect to property (1): it is known that mu-calculus is (equivalent to) the largest fragment of monadic second-order logic which is invariant under bisimulation.

In this talk, I will define a class of logics, called "update logics". The name comes from the fact that some versions of these logics were first introduced in my previous work on "epistemic actions", i.e. as logics to model the updating of information in multi-agent systems (joint work with L. Moss and S. Sloecki). Here I stick with a different interpretation of these formalisms, as logics for "updating" or "controlling" a transition system. As such, the "action modalities" can be understood to model a class of "program transformations", which preserve bisimilarity.

I give examples of update formulas and their interpretations and models, I show all these logics are invariant under bisimulation, but some of them cannot be embedded in mu-calculus (and hence, by the above result, cannot be embedded in monadic second-order logic either). I present a proof system and I sketch an attempt to show completeness and decidability for some fragments of this logic. The general completeness and decidability problem is open.