Starting originally from my previous work on formalizing "epistemic actions" (joint work with L. Moss and S. Solecki), I have been recently working on logics for process transformations. A process transformation is a partial map from processes to processes, with the property that it's bisimulation-preserving: bisimilar processes are mapped to bisimilar processes. Some transformations can be considered themselves as processes, by endowing them with a transition structure in a natural way: I call these process updates.

A modal logic for processes is a logic describing unary properties (predicates) of processes which are bisimulation-invariant: this means such properties are preserved under bisimulation. Standard modal logic, PDL, mu-calculus, various extensions of PDL are examples of such logics. All such logics must be based on modalities which are "safe for bisimulation": when applied to bisimulation-invariant predicates, they should yield bisimulation-invariant properties. I show that any process transformation can be used to produce such a modality. I give examples of non-standard modal logics which arise in this way: e.g. "update logics" correspond to update transformations. I show that some update modalities are not definable in mu-calculus, or in any logic with a "classical"-style semantics, due to their lack of what I call "strong compositionality": their semantics is essentially based on "doing things to processes" and not just on "what processes do to things".

I put all this into a coalgebraic perspective, defining all the above notions, first for a particular simple notion of process, and then in general for the abstract notion of processes as F-coalgebras, for an arbitrary functor F. Process transformations are functors on the category of pointed coalgebras, while process logics are logics for which the truth-map is a functor. I put these notions in the general perspective on "coalgebraic modalities as natural transformations" based on "predicate-lifting", provided by the work of A. Kurz and D. Pattinson. I compare my notions with theirs, first generalizing it to a notion of "natural predicate transformers", which is closed under all natural operations with modalities. I show that my notion of modal predicates is essentially the same as theirs, while our notions of modality differ. I further generalize this notion to "natural predicate updates", which captures update modalities coagebraically.