Coalgebraic Logic and Synthesis of Mealy Machines

Abstract. 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.

• Type: Conference
• Year: 2008
• Where: FOSSACS
• Authors: Marcello M. Bonsangue, Jan J. M. M. Rutten, Alexandra Silva
• Keywords: Deterministic Mealy Machines, Finite Mealy Machine, FOSSACS 2008, Mealy Machine, Software Engineering