Speaker
Description
Frits Vaandrager and Thorsten Wißmann
Abstract: 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 R, we introduce a contraction operator α_R that turns a low-level model M into a high-level model, and a refinement operator ϱ_R that transforms a high-level model N into a low-level model. We establish a Galois connection ϱ_R (N) ⊑ M ⇔ N ⊑ α_R(M), where ⊑ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model M. To this end, we also introduce a concretization operator γ_R , which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection α_R (M) ⊑ N ⇔ M ⊑ γ_R(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 M models a black-box system then α_R (M) describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code R. Whenever α_R (M) implements (or conforms to) N, we may conclude that M implements (or conforms to) γ_R(N).