一句话：在互模拟语义下重新刻画下推自动机与上下文无关文法的对应，指出需引入状态感知才能恢复完整对应。
经典自动机理论通常以语言等价刻画下推自动机与上下文无关文法的对应，但面向交互计算的 Reactive Turing Machine 使用带标签迁移和进程图，并以互模拟而非语言等价作为行为等价。本文在互模拟语义下重新考察这一经典对应。作者把进程代数中的顺序组合算子改为一种带中间接受的顺序算子，使两者在进程图层面的对应更精确；进一步分析表明，要恢复完整的对应关系，还需引入状态感知（state awareness）这一概念。结果表明，在交互式/进程语义中，传统对应并非直接成立，而依赖于算子设计与状态可见性。
The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence. Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness.
@article{paperbot2234,
title = {Pushdown Automata and Context-Free Grammars in Bisimulation Semantics},
author = {Jos C. M. Baeten and Cesare Carissimo and Bas Luttik},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:15)2023}
}