Action Codes

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 action codes, a variation of the prefix codes known from coding theory. For each action code $\mathcal{R}$, we introduce a contraction operator $\alpha_\mathcal{R}$ that turns a low-level model $M$ into a high-level model, and a refinement operator $\varrho_\mathcal{R}$ that transforms a high-level model $N$ into a low-level model. We establish a Galois connection $\varrho_\mathcal{R}(N) \sqsubseteq M \Leftrightarrow N \sqsubseteq \alpha_\mathcal{R}(M)$, where $\sqsubseteq$ denotes the well-known simulation preorder. In practice, we typically want to obtain an overapproximation of model $M$. To this end, we also introduce a concretization operator $\gamma_\mathcal{R}$. This operator behaves like the refinement operator, but adds arbitrary behavior at intermediate points during a refinement. We establish a second Galois connection $\alpha_\mathcal{R}(M) \sqsubseteq N \Leftrightarrow M \sqsubseteq \gamma_\mathcal{R}(N)$. We show how an action code may be used to construct an adaptor that translates between concrete and abstract inputs and outputs during learning and conformance testing of a black-box system. If $M$ models a black-box system then $\alpha_\mathcal{R}(M)$ describes the behavior that can be observed by a tester/learner that interacts with this system via an adaptor derived from code $\mathcal{R}$. Whenever we have established that $\alpha_\mathcal{R}(M)$ implements (or conforms to) $N$, we may conclude that $M$ implements (or conforms to) $\gamma_{\mathcal{R}} (N)$.