DROPS

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2023.137

Action Codes

Authors: Frits Vaandrager and Thorsten Wißmann

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

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 ℛ, 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.

Cite as

Frits Vaandrager and Thorsten Wißmann. Action Codes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 137:1-137:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vaandrager_et_al:LIPIcs.ICALP.2023.137,
  author =	{Vaandrager, Frits and Wi{\ss}mann, Thorsten},
  title =	{{Action Codes}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{137:1--137:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.137},
  URN =		{urn:nbn:de:0030-drops-181895},
  doi =		{10.4230/LIPIcs.ICALP.2023.137},
  annote =	{Keywords: Automata, Models of Reactive Systems, LTS, Action Codes, Action Refinement, Action Contraction, Galois Connection, Model-Based Testing, Model Learning}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.ICALP.2019.4

Automata Learning and Galois Connections (Invited Talk)

Authors: Frits Vaandrager

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract

Automata learning is emerging as an effective technique for obtaining state machine models of software and hardware systems. I will present an overview of recent work in which we used active automata learning to find standard violations and security vulnerabilities in implementations of network protocols such as TCP and SSH. Also, I will discuss applications of automata learning to support refactoring of legacy control software and identifying job patterns in manufacturing systems. As a guiding theme in my presentation, I will show how Galois connections (adjunctions) help us to scale the application of learning algorithms to practical problems.

Cite as

Frits Vaandrager. Automata Learning and Galois Connections (Invited Talk). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{vaandrager:LIPIcs.ICALP.2019.4,
  author =	{Vaandrager, Frits},
  title =	{{Automata Learning and Galois Connections}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.4},
  URN =		{urn:nbn:de:0030-drops-105800},
  doi =		{10.4230/LIPIcs.ICALP.2019.4},
  annote =	{Keywords: Automaton Learning, Model Learning, Protocol Verification, Applications of Automata Learning, Galois Connections}
}

Document

DOI: 10.4230/DagSemRep.156

Expressiveness in Concurrency (Dagstuhl Seminar 9638)

Authors: Rocco De Nicola, Ursula Goltz, and Frits Vaandrager

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

Rocco De Nicola, Ursula Goltz, and Frits Vaandrager. Expressiveness in Concurrency (Dagstuhl Seminar 9638). Dagstuhl Seminar Report 156, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)

Copy BibTex To Clipboard

@TechReport{denicola_et_al:DagSemRep.156,
  author =	{De Nicola, Rocco and Goltz, Ursula and Vaandrager, Frits},
  title =	{{Expressiveness in Concurrency (Dagstuhl Seminar 9638)}},
  pages =	{1--7},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{156},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.156},
  URN =		{urn:nbn:de:0030-drops-150438},
  doi =		{10.4230/DagSemRep.156},
}

Search Results

Documents authored by Vaandrager, Frits

Action Codes

Abstract

Cite as

Automata Learning and Galois Connections (Invited Talk)

Abstract

Cite as

Expressiveness in Concurrency (Dagstuhl Seminar 9638)

Abstract

Cite as

Thanks for your feedback!

Could not send message