Effectful Mealy Machines

TL;DR

This paper introduces effectful Mealy machines, a generalized model incorporating global effects, and provides semantics based on bisimilarity and traces, connecting to causal processes and monoidal causal functions.

Contribution

It generalizes Mealy machines with global effects and offers a unified semantic framework for bisimilarity and trace equivalence, including a monoidal extension.

Findings

Characterizes standard causal processes.

Defines effectful Mealy machines with semantics.

Introduces monoidal causal processes.

Abstract

Effectful Mealy machines, which we introduce, are a generalization of Mealy machines with global effects determined by an effectful triple. We provide semantics of effectful Mealy machines in terms of both bisimilarity and traces: bisimilarity is characterized syntactically, via uniform feedback; traces are constructed coinductively in terms of streams. We prove that this framework characterizes standard causal processes and existing flavours of Mealy machine, bisimilarity, and trace equivalence. In the commutative case, we introduce a monoidal generalization of Raney's causal functions: monoidal causal processes.