eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-05
137:1
137:20
10.4230/LIPIcs.ICALP.2023.137
article
Action Codes
Vaandrager, Frits
1
https://orcid.org/0000-0003-3955-1910
Wißmann, Thorsten
1
2
https://orcid.org/0000-0001-8993-6486
Radboud University, Nijmegen, The Netherlands
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
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 ℛ, we introduce a contraction operator α_ℛ that turns a low-level model ℳ into a high-level model, and a refinement operator ϱ_ℛ that transforms a high-level model 𝒩 into a low-level model. We establish a Galois connection ϱ_ℛ(𝒩) ⊑ ℳ ⇔ 𝒩 ⊑ α_ℛ(ℳ), where ⊑ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model ℳ. To this end, we also introduce a concretization operator γ_ℛ, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection α_ℛ(ℳ) ⊑ 𝒩 ⇔ ℳ ⊑ γ_ℛ(𝒩). 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 ℳ models a black-box system then α_ℛ(ℳ) describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code ℛ. Whenever α_ℛ(ℳ) implements (or conforms to) 𝒩, we may conclude that ℳ implements (or conforms to) γ_ℛ (𝒩).
Almost all results, examples, and counter-examples are formalized in Coq.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol261-icalp2023/LIPIcs.ICALP.2023.137/LIPIcs.ICALP.2023.137.pdf
Automata
Models of Reactive Systems
LTS
Action Codes
Action Refinement
Action Contraction
Galois Connection
Model-Based Testing
Model Learning