Koalgebraische Semantik und Minimierung in Mengen und ...re06huxa/defense-talk... · Semantik...

Koalgebra CTS Nominelle Mengen Minimalitätsbegriff Erreichbarkeit Verhaltensäquivalenz 1 / 16

Koalgebraische Semantik und Minimierungin Mengen und darüber hinaus

Coalgebraic Semanticsand Minimizationin Sets and Beyond

Thorsten Wißmann3. Juni 2020

FAU Erlangen-Nürnberg

Semantik

Minimierung

Kapitel 2Standard-Literatur

Kapitel 5Erreichbarkeit

Kapitel 6Verhaltensäquivalenz

Kapitel 7Minimalitäts-

begriff

Koalgebren in Mengen und darüber hinaus

Kapitel 4Conditional Transition Systems

Kapitel 3Orbit-Endliche Verhalten

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

Funktor F ∶C → C F -Koalgebra

F -Koalgebra-HomomorphismusBeispiel

P2 × (−)A

R(−)

F ∶PosF ∶Nom

F ∶Set→ Set c∶C

Zustandsmenge

→ FC

h∶ (C , c)→ (D, d)Semantik / Verhaltensäquivalenz:3a

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

c∶C → PC

„Transitionssystem“

h∶ (C , c)→ (D, d)Semantik / Verhaltensäquivalenz:

„Bisimilarität“3a5b

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

c∶C → 2 × CA

„Determin. Automat“

„Sprach-Äquivalenz“

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

c∶C → R(C)„Markov-Kette“

„Gewichtete Bisimil.“3a5b

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

c∶C → FXΦ

„CTS“

„Conditional Bisim.“3a5b

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

8a3b 4a

P2 × (−)A

R(−)

F ∶PosF ∶Nom

Zustandsmenge

→ FC

c∶C → FX

„Equivariant“

„(α-)Äquiv.-Klassen“3a5b

8a3b 4a

Instanzen vonF -Koalgebren

KoalgebraischeErgebnisse

Transitionssysteme

Deterministische Automaten

Markov-Ketten

Koinduktions-Prinzip

Algorithmen

Neue Instanz Neue Methode

Transitionssysteme

Markov-Ketten

Algorithmen

Transitionssysteme

Markov-Ketten

Algorithmen

Transitionssysteme

Markov-Ketten

Algorithmen

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

Definition für halbgeordnete Menge (Φ,≤) Versionen

• Conditional Transition System:f ∶C → Pos((Φ,≤), (PC ,⊇))

• Conditional Bisimulation:Bisimulationen (Rφ)φ∈Φ, ...., monoton in φ.

[Beohar, König, Küpper, Silva, 2017]

yv1, v2

v1, v2

Verallgemeinerte Definitionen für F ∶Pos → Pos• F hat Versionsfilter ∣φ∶FX → FX (in K̀ ((−)Φ)), wenn ....• Conditional Bisimulation auf c∶C → FCΦ:

Bisimulationen (Rφ)φ∈Φ, ... , monoton in φ

Theorem Für sog. Upgrade-erhaltende c∶C → FCΦ gilt:Conditional Bisimilarity = Koalgebraische Verhaltensäquivalenz

Neue Instanz

yv1, v2

v1, v2

Neue Instanz

yv1, v2

v1, v2

Neue Instanz

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

Kategorie der Nominellen Mengen• Elemente halten endlich viele Atome

freie Variablen

von A = {a0

(Variablen-)Namen

, a1, . . .}• Formalisiert Umbenennen, Allozieren, Binden von Namen:

λx .x =α λy .y ≠α λx .y

KoalgebrenAutomaten für unendliches Eingabealphabet A (z.B. FX = 2×XA)Termbäume mit Bindung (z.B. FX

λ-Bäume= A + X × X + [A]Bindungs-Funktor

Theorem Für F ∶∶= NKonstant ∣ F + F ∣ F × F ∣ Pf ∣ A ∣ [A](−) ∣ (−)A:

Orbit-endlicheF -Koalgebren =

Quotient von endlichenF ′-Koalgebren in Mengen

(z.B. α-Äquivalenzklassen) Neues Ergebnis

Nominelle Mengen(Endlicher Support)

Orbit-endliche Verhalten(Rationaler Fixpunkt)

Unendliche Verhalten(Finale Koalgebra)↯↯♥♥

freie Variablen

von A = {a0

(Variablen-)Namen

freie Variablen

von A = {a0

(Variablen-)Namen

freie Variablen

von A = {a0

(Variablen-)Namen

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

MinimierenReduzieren der Zustände

bei gleicher Semantik

ErreichbarkeitUnerreichbare

ZuständeEntfernen

VerhaltensäquivalenzZustände

gleichen VerhaltensVerschmelzen

Kategorielle GemeinsamkeitenEindeutigkeit, Existenz

Aber: Algorithmisch verschieden!

ZuständeEntfernen

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

Punktierte Unterkoalgebra

1 C FC

C ′ FC ′

x ′0

von (C , f , x0)Definition Erreichbarer Teil

von (C , f , x0) = Kleinste punktierteUnterkoalgebra

Theorem Wenn F unendliche Schnitteschwache Bedingung

erhält und die Kategorieein Faktorisierungssystem hat:• Iterative Konstruktion (höchstens abzählbar viele Schritte).• Konstruktion ist funktoriell, wenn F Urbilder erhält.

Methode

In Mengen:Breitensuche auf

kanonischem Graph.

In Kleisli-Kategorien:Annahmen manchmal

erfüllt.

Reduktion

1 C FC

C ′ FC ′

x ′0

Methode

kanonischem Graph.

erfüllt.

Reduktion

1 C FC

C ′ FC ′

x ′0

Methode

kanonischem Graph.

erfüllt.

Reduktion

Semantik

Minimierung

begriff

Semantik

Minimierung

begriff

VerhaltensäquivalenzGegeben:

c∶C → FC

Gesucht: kleinster Quotient (D, d) /C FC

Koalgebraischer Algorithmus

für Verhaltensäquivalenz

DeterministischeDeterministischeendl. Automatenendl. Automaten

n ⋅ log nn ⋅ log n ∣A∣ ⋅ n ⋅ log n∣A∣ ⋅ n ⋅ log nHopcroft ’71Hopcroft ’71 Gries ’73Gries ’73

Knuutila ’01Knuutila ’01(Gelabelte)(Gelabelte)

Transitions-SystemeTransitions-Systemem ⋅ log nm ⋅ log n

Paige, Tarjan ’87Paige, Tarjan ’87Valmari ’09Valmari ’09

Gewichtete SystemeGewichtete Systeme“Markov Chain Lumping”“Markov Chain Lumping”

m ⋅ log nm ⋅ log nValmari, Franceschinis ’10Valmari, Franceschinis ’10

Segala-SystemeSegala-Systememdist ⋅ log mactsmdist ⋅ log macts

Groote, Verduzco,Groote, Verduzco,de Vink ’18de Vink ’18

GewichteteGewichteteBaumautomatenBaumautomatenm ⋅ nm ⋅ n // m ⋅ log nm ⋅ log nHögberg, Maletti,Högberg, Maletti,

May ’07May ’07

ÄhnlicherAblauf Ähnliche

Laufzeit

System-Typ fest-verdrahtet

May ’07May ’07

Laufzeit

May ’07May ’07

Laufzeit

May ’07May ’07

Laufzeit

May ’07May ’07

Laufzeit

May ’07May ’07

Laufzeit

May ’07May ’07

Laufzeit

Neue Methode

Konstruktion des kleinsten Quotienten von c∶C → FC inKategorie mit (RegEpi,Mono)-Faktorisierungssystem

Partitionen: Pi ≤ Qi auf C , werden schrittweise verfeinertHeuristik: Welche Information wird als Nächstes weiterver-arbeitet?• Alles gleichzeitig ⇒ Qi+1 = Pi

„Final Chain Algorithmus“ [König, Küpper ’14]• „Smaller half“ ⇒ S ∈ C/Pi B ∈ C/Qi S ⊆ B mit

∣S∣ ≤ 12 ⋅ ∣B∣

Optimierung für Koalgebren in Set:Inkrementelle Berechnung der Partitionen

Wenn F zippable, d.h. wenn

F(A + B)⟶ F(A + 1) × F(1 + B) injektiv

dann: Qi+1 = Qi ∩ kerχBS Pi+1 = Pi ∩ ker(χB

S ⋅ c)(zippable nicht abgeschlossen unter: Komposition, Quotient)

Pseudocode für Verfeinerungs-Schritt,Refinement-Interface für Funktor-Spezifisches

Encoding: ♭∶FX → B(A × X)Refinement-Interface für F :init∶F1→ BA→Wupdate∶BA ×W →W × F3 ×W

Korrektheit: w ∶PX → (FX →W ). . . . . .

a1 a2 a3 a4 a5 a6

S B \ S

Laufzeitanalyse: O(mKanten

⋅ log nZustände) für F ∈ {Pf, M(−), R(−), B, Σ}

Laufzeit: O((m + n) ⋅ log n ⋅ p(C , c))Fast immer: m ≥ nLaufzeit-Parameter p(C , c) des Refinement Interfaces:p(C , c) = log min(∣M∣,m) für M(−) wenn M nicht kürzbarp(C , c) = maxσ∈Σ ar(σ) für Polynomialfunktor Σp(C , c) = 1 sonst

Modularität: Kombination der Funktoren via: +, ×, ◦

Vorverarbeitung durch Erzeugen von Zwischenzuständen:(F ◦ G)-Koalgebren ↝ (F + G)-KoalgebrenKonstruktion in extensiver Kategorie

Implementierung: CoPaRKombinierter Set-Funktor F

F -Koalgebra }⟹ Verhaltensäquivalenz

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Systemtyp Funktor FX Laufzeit (m ≥ n) Maßgeschneiderter Algorithmus

Transitions-Systeme PfX m ⋅ log n = m ⋅ log n Paige, Tarjan 1987

LTS Pf(N × X) m ⋅ log m = m ⋅ log m Dovier, Piazza, Policriti 2004

> m ⋅ log n Valmari 2009

Markov-Ketten R

(X) m ⋅ log n = m ⋅ log n Valmari, Franceschinis 2010

Determi-nistischeAutomaten

2 × XA (A fest) n ⋅ log n = n ⋅ log n Hopcroft 1971

2 ×Pf(A × X) ∣A∣ ⋅ n ⋅ log n = ∣A∣ ⋅ n ⋅ log n Gries 1973/Knuutila 2001

SegalaSysteme Pf(A ×DX) mD ⋅ log mPf

< m ⋅ log n Baier, Engelen,Majster-Cederbaum 2000

= mD ⋅ log mPf Groote, Verduzco, de Vink 2018

ColourRefinement BX = N(X) m ⋅ log n = m ⋅ log n Berkholz, Bonsma, Grohe 2017

GewichteteBaum-Automaten(BackwardsBisimulation)

M(ΣX) Neu

M nicht kürzbarm ⋅ log2 m < m ⋅ n Högberg, Maletti, May 2007

M(ΣX)M kürzbar

m ⋅ log m =Σ fest

m ⋅ log n Högberg, Maletti, May 2007

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Markov-Ketten R

M(ΣX) Neu

M(ΣX)M kürzbar

Markov-Ketten R

M(ΣX) Neu

M(ΣX)M kürzbar

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

Neue Methode

∣S∣ ≤ 12 ⋅ ∣B∣

a1 a2 a3 a4 a5 a6

S B \ S

NeueInstanzen

NeueMethoden

NeueErgebnisse

ConditionalTransitionSystems

GewichteteBaum-

Automaten

Weitere?

Erreichbarkeit:Konstruktion& Reduktion

Verhaltensäquivalenz:Generischer & Modularer

m ⋅ log n Algorithmusfür Partition Refinement

Weitere?

Gemeinsamkeitenzwischen

Minimierungs-aspekten

Orbit-endlicheKoalgebren in

Nominellen Mengen

Weitere?

Koalgebra CTS Nominelle Mengen Minimalitätsbegriff Erreichbarkeit Verhaltensäquivalenz ∞ / 16

Christoph Berkholz, Paul S. Bonsma, Martin Grohe.“Tight Lower and Upper Bounds for the Complexityof Canonical Colour Refinement”. In: TheoryComput. Syst. 60.4 (2017), S. 581–614. doi:10.1007/s00224-016-9686-0. url: https://doi.org/10.1007/s00224-016-9686-0.Christel Baier, Bettina Engelen,Mila Majster-Cederbaum. “Deciding Bisimilarity andSimilarity for Probabilistic Processes”. In: J.Comput. Syst. Sci. 60 (2000), S. 187–231.Harsh Beohar, Barbara König, Sebastian Küpper,Alexandra Silva. “Conditional Transition Systemswith Upgrades”. In: 11th International Symposiumon Theoretical Aspects of Software Engineering(TASE 2017) (2017). Full version available athttps://arxiv.org/abs/1706.02526.

Harsh Beohar, Barbara König, Sebastian Küpper,Alexandra Silva, Thorsten Wißmann. “A coalgebraictreatment of conditional transition systems withupgrades”. In: Logical Methods in ComputerScience Volume 14, Issue 1 (Feb. 2018). doi:10.23638/LMCS-14(1:19)2018. url:https://lmcs.episciences.org/4330/pdf.Ulrich Dorsch, Stefan Milius, Lutz Schröder,Thorsten Wißmann. “Efficient Coalgebraic PartitionRefinement”. In: Proc. 28th InternationalConference on Concurrency Theory (CONCUR2017). LIPIcs. Schloss Dagstuhl - Leibniz-Zentrumfuer Informatik, 2017. doi:10.4230/LIPIcs.CONCUR.2017.32. url:https://drops.dagstuhl.de/opus/volltexte/2017/7793/.

Agostino Dovier, Carla Piazza, Alberto Policriti. “Anefficient algorithm for computing bisimulationequivalence”. In: Theor. Comput. Sci. 311.1-3(2004), S. 221–256.David Gries. “Describing an algorithm by Hopcroft”.In: Acta Informatica 2 (1973), S. 97–109. issn:1432-0525.Jan Friso Groote, Jao Rivera Verduzco,Erik P. de Vink. “An Efficient Algorithm toDetermine Probabilistic Bisimulation”. In:Algorithms 11.9 (2018), S. 131. doi:10.3390/a11090131. url:https://doi.org/10.3390/a11090131.

Johanna Högberg, Andreas Maletti, Jonathan May.“Bisimulation Minimisation for Weighted TreeAutomata”. In: Developments in Language Theory,DLT 2007. Bd. 4588. LNCS. Springer, 2007,S. 229–241. isbn: 978-3-540-73207-5. doi:10.1007/978-3-540-73208-2. url: https://doi.org/10.1007/978-3-540-73208-2.John Hopcroft. “An n log n algorithm for minimizingstates in a finite automaton”. In: Theory ofMachines and Computations. Academic Press, 1971,S. 189–196.Barbara König, Sebastian Küpper. “GenericPartition Refinement Algorithms for Coalgebras andan Instantiation to Weighted Automata”. In:Theoretical Computer Science, IFIP TCS 2014.Bd. 8705. LNCS. Springer, 2014, S. 311–325. isbn:978-3-662-44601-0.

Timo Knuutila. “Re-describing an algorithm byHopcroft”. In: Theor. Comput. Sci. 250 (2001),S. 333–363. issn: 0304-3975.Robert Paige, Robert E. Tarjan. “Three partitionrefinement algorithms”. In: SIAM J. Comput. 16.6(1987), S. 973–989.Antti Valmari. “Bisimilarity Minimization inO(m log n) Time”. In: Applications and Theory ofPetri Nets, PETRI NETS 2009. Bd. 5606. LNCS.Springer, 2009, S. 123–142. isbn:978-3-642-02423-8.Antti Valmari, Giuliana Franceschinis. “SimpleO(m log n) Time Markov Chain Lumping”. In: Toolsand Algorithms for the Construction and Analysis ofSystems, TACAS 2010. Bd. 6015. LNCS. Springer,2010, S. 38–52.

Thorsten Wißmann, Ulrich Dorsch, Stefan Milius,Lutz Schröder. “Efficient and Modular CoalgebraicPartition Refinement”. In: Logical Methods inComputer Science Volume 16, Issue 1 (Jan. 2020).doi: 10.23638/LMCS-16(1:8)2020. url:https://lmcs.episciences.org/6064.Thorsten Wißmann, Stefan Milius,Shin-ya Katsumata, Jérémy Dubut. “A CoalgebraicView on Reachability”. In: CommentationesMathematicae Universitatis Carolinae 60, 4 (Dez.2019), S. 605–638.

Koalgebraische Semantik und Minimierung in Mengen und ...re06huxa/defense-talk... · Semantik...

Documents

Transcript of Koalgebraische Semantik und Minimierung in Mengen und ...re06huxa/defense-talk... · Semantik...