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.
, , ,
Software Engineering [SEN]
Computer Security

Bonsangue, M.M, Rutten, J.J.M.M, & Silva, A.M. (2007). Coalgebraic logic and synthesis of Mealy machines. Software Engineering [SEN]. CWI.