Action Codes
Vaandrager F, Wißmann T (2023)
Publication Type: Conference contribution
Publication year: 2023
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 261
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Paderborn, DEU
ISBN: 9783959772785
DOI: 10.4230/LIPIcs.ICALP.2023.137
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). Almost all results, examples, and counter-examples are formalized in Coq.
Authors with CRIS profile
Involved external institutions
Netherlands (NL)How to cite
APA:
Vaandrager, F., & Wißmann, T. (2023). Action Codes. In Kousha Etessami, Uriel Feige, Gabriele Puppis (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Paderborn, DEU: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Vaandrager, Frits, and Thorsten Wißmann. "Action Codes." Proceedings of the 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, Paderborn, DEU Ed. Kousha Etessami, Uriel Feige, Gabriele Puppis, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2023.
BibTeX: Download