We present a novel coalgebraic logic for deterministic Mealy machines that is sound, complete and expressive w.r.t. bisimulation.
Every finite Mealy machine corresponds to a finite formula in the language. For the converse, we give a compositional synthesis
algorithm which transforms every formula into a finite Mealy machine whose behaviour is exactly the set of causal functions
satisfying the formula.