Effectful Mealy Machines, Bisimulation and Trace (Bonchi, Di Lavore, Román, 2025)

Abstract

We introduce effectful Mealy machines - a general notion of Mealy machine with global effects - and give them semantics in terms of both bisimilarity and traces. Bisimilarity of effectful Mealy machines is characterized syntactically, via free uniform feedback. Traces of effectful Mealy machines are given a novel semantic coinductive universe in terms of effectful streams. We prove that this framework generalizes standard causal processes and captures existing flavours of Mealy machine, bisimilarity, and trace.

(https://arxiv.org/abs/2410.10627)

@article{bdr25:mealy,
  author       = {Filippo Bonchi and
                  Elena {Di Lavore} and
                  Mario Rom{\'{a}}n},
  title        = {Effectful Mealy Machines: Bisimulation and Trace},
  journal      = {CoRR},
  volume       = {abs/2410.10627},
  year         = {2024},
  doi          = {10.48550/ARXIV.2410.10627},
  note = {To appear in the 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'25)},
}

• Raw effectful machine