一句话：提出带全局效应的 Mealy 机，以自由一致反馈刻画互模拟，并用带效应流建立迹的余代数语义。
论文引入带效应的 Mealy 机（effectful Mealy machines），将经典 Mealy 机推广到具有全局效应的情形，并为其建立互模拟与迹两种语义。互模拟通过自由一致反馈（free uniform feedback）给出语法刻画；迹则被赋予一种新的语义余代数宇宙，即带效应流（effectful streams）。作者证明该框架能推广标准因果过程，并统一捕获已有的 Mealy 机、互模拟与迹的多种变体，从而为效应与反馈下的交互系统提供统一的语义基础。
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.
DOI 原文 ·
@inproceedings{paperbot8644,
title = {Effectful Mealy Machines: Bisimulation and Trace},
author = {Filippo Bonchi and Elena Di Lavore and Mario Román},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00047}
}