We provide a new perspective on the problem how high-level state machine models with abstract actions can be related to low-level models in which these actions are refined by sequences of concrete actions. We describe the connection between high-level and low-level actions using \emph{action codes}, a variation of the prefix codes known from coding theory. For each action code ${\mathcal{R}}$, we introduce a \emph{contraction} operator $\alpha_{\mathcal{R}}$ that turns a low-level model $\mathcal{M}$ into a high-level model, and a \emph{refinement} operator $\rho_{\mathcal{R}}$ that transforms a high-level model $\mathcal{N}$ into a low-level model. We establish a Galois connection $\rho_{\mathcal{R}}(\mathcal{N}) \sqsubseteq \mathcal{M} \Leftrightarrow \mathcal{N} \sqsubseteq \alpha_{\mathcal{R}}(\mathcal{M})$, where $\sqsubseteq$ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model $\mathcal{M}$. To this end, we also introduce a \emph{concretization} operator $\gamma_{\mathcal{R}}$, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection $\alpha_{\mathcal{R}}(\mathcal{M}) \sqsubseteq \mathcal{N} \Leftrightarrow \mathcal{M} \sqsubseteq \gamma_{\mathcal{R}}(\mathcal{N})$. Action codes may be used to construct adaptors that translate between concrete and abstract actions during learning and testing of Mealy machines. If Mealy machine $\mathcal{M}$ models a black-box system then $\alpha_{\mathcal{R}}(\mathcal{M})$ describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code ${\mathcal{R}}$. Whenever $\alpha_{\mathcal{R}}(\mathcal{M})$ implements (or conforms to) $\mathcal{N}$, we may conclude that $\mathcal{M}$ implements (or conforms to) $\gamma_{{\mathcal{R}}} (\mathcal{N})$.

翻译：针对具有抽象动作的高层状态机模型如何与通过具体动作序列精化这些动作的低层模型相关联的问题，我们提出一种新视角。利用编码理论中前缀码的变体——\emph{动作码}，描述高层与低层动作间的关联。针对每个动作码${\mathcal{R}}$，引入\emph{压缩}算子$\alpha_{\mathcal{R}}$（将低层模型$\mathcal{M}$转化为高层模型）与\emph{精化}算子$\rho_{\mathcal{R}}$（将高层模型$\mathcal{N}$转化为低层模型），并建立伽罗瓦连接$\rho_{\mathcal{R}}(\mathcal{N}) \sqsubseteq \mathcal{M} \Leftrightarrow \mathcal{N} \sqsubseteq \alpha_{\mathcal{R}}(\mathcal{M})$（其中$\sqsubseteq$为经典的模拟预序）。为满足一致性验证需求（通常需获得模型$\mathcal{M}$的过近似），进一步引入\emph{具体化}算子$\gamma_{\mathcal{R}}$——该算子行为类似精化算子，但会在中间点添加任意行为，从而形成第二组伽罗瓦连接$\alpha_{\mathcal{R}}(\mathcal{M}) \sqsubseteq \mathcal{N} \Leftrightarrow \mathcal{M} \sqsubseteq \gamma_{\mathcal{R}}(\mathcal{N})$。动作码可用于构建适配器，在Mealy机学习与测试过程中实现具体动作与抽象动作的转换。若Mealy机$\mathcal{M}$建模黑箱系统，则$\alpha_{\mathcal{R}}(\mathcal{M})$描述了通过源自码${\mathcal{R}}$的适配器与该系统交互的学习者/测试者所能观测的行为。当$\alpha_{\mathcal{R}}(\mathcal{M})$实现（或符合）$\mathcal{N}$时，可推导出$\mathcal{M}$实现（或符合）$\gamma_{{\mathcal{R}}} (\mathcal{N})$。