Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 
Startseite    Anmelden     
Logout in [min] [minutetext]

Quantitatives Model Checking - Einzelansicht

Grunddaten
Veranstaltungsart V/Ü Langtext
Veranstaltungsnummer 100092 Kurztext
Semester WiSe 2022/23 SWS 4
Erwartete Teilnehmer/-innen 40 Studienjahr
Max. Teilnehmer/-innen 40
Credits Belegung Belegpflicht
Hyperlink
Weitere Links Learnweb-Kurs (Einschreibeschlüssel: QMC)
Sprache deutsch
Termine Gruppe: [unbenannt] iCalendar Export für Outlook
  Tag Zeit Rhythmus Dauer Raum Raum-
plan
Lehrperson Status Bemerkung fällt aus am Max. Teilnehmer/-innen
Einzeltermine anzeigen
iCalendar Export für Outlook
Mo. 14:00 bis 16:00 woch 10.10.2022 bis 23.01.2023  Einsteinstr. 64 - M B 6 (M 6)        
Einzeltermine anzeigen
iCalendar Export für Outlook
Do. 14:00 bis 16:00 woch 13.10.2022 bis 26.01.2023  Einsteinstr. 64 - M B 6 (M 6)        
Gruppe [unbenannt]:
 


Zugeordnete Personen
Zugeordnete Personen Zuständigkeit
Remke, Anne, Prof. Dr. verantwort
Niehage, Mathis verantwort
Blohm, Pauline begleitend
Studiengänge
Abschluss - Studiengang Sem ECTS Bereich Teilgebiet
Master - Mathematics (88 F23 20) -
Master - Informatik (88 079 20) -
Zwei-Fach-Bachelor - Informatik (L2 079 11) -
Bachelor - Informatik (82 079 7) - 6
Master - Mathematik (88 105 10) - 6
Bachelor - Informatik (82 079 11) - 6
Master - Mathematik (88 105 13) -
Master - Informatik (88 079 8) - 6
Master - Informatik (88 079 14) -
MEd Gymnasien u Gesamt - Informatik (E3 079 19) -
Prüfungen / Module
Prüfungsnummer Modul
14101 Vorlesung - MEd Gymnasien u Gesamt Informatik Version 2019
14102 Übungen zur gewählten Vorlesung - MEd Gymnasien u Gesamt Informatik Version 2019
13101 Vorlesung 1 - MEd Gymnasien u Gesamt Informatik Version 2019
13102 Übungen zur gewählten Vorlesung 1 - MEd Gymnasien u Gesamt Informatik Version 2019
13103 Vorlesung 2 - MEd Gymnasien u Gesamt Informatik Version 2019
13104 Übungen zur gewählten Vorlesung 2 - MEd Gymnasien u Gesamt Informatik Version 2019
436002 Übungen zu "Ergänzungsvorlesung Formale Methoden" - Master Mathematics Version 2020
29002 Übungen zu "Ergänzungsvorlesung Formale Methoden" - Master Informatik Version 2020
31002 Übungen zu "Ergänzungsvorlesung Formale Methoden" - Master Informatik Version 2020
30002 Übungen zu "Ergänzungsvorlesung Formale Methoden" - Master Informatik Version 2020
437002 Übungen zu "Ergänzungsvorlesung Formale Methoden" - Master Mathematics Version 2020
17001 Vorlesungen aus dem Vorlesungsangebot der Informatik 1 - Bachelor Informatik Version 2011
27001 Vorlesung (mit integrierter oder separater Übung) - Master Informatik Version 2014
16001 eine Vorlesung oder eine Vorlesung mit Übungen aus dem Wahlpflicht-Vorlesungsangebot des Instituts für Informatik - Zwei-Fach-Bachelor Informatik Version 2011
18001 Vorlesungen aus dem Vorlesungsangebot der Informatik 1 - Bachelor Informatik Version 2011
28001 Vorlesung (mit integrierter oder separater Übung) - Master Informatik Version 2014
29001 Vorlesung (mit integrierter oder separater Übung) - Master Informatik Version 2014
2013001 Vorlesung (mit integrierter oder separater Übung) - Master Mathematik Version 2013
2014001 Vorlesung (mit integrierter oder separater Übung) - Master Mathematik Version 2013
2015001 Vorlesung (mit integrierter oder separater Übung) - Master Mathematik Version 2013
16010 Modulabschlussprüfung - Zwei-Fach-Bachelor Informatik Version 2011
30001 Ergänzungsvorlesung Formale Methoden - Master Informatik Version 2020
29001 Ergänzungsvorlesung Formale Methoden - Master Informatik Version 2020
31001 Ergänzungsvorlesung Formale Methoden - Master Informatik Version 2020
437001 Ergänzungsvorlesung Formale Methoden - Master Mathematics Version 2020
436001 Ergänzungsvorlesung Formale Methoden - Master Mathematics Version 2020
438002 Übungen zu "Ergänzungsvorlesung Formale Methoden" - Master Mathematics Version 2020
438001 Ergänzungsvorlesung Formale Methoden - Master Mathematics Version 2020
Prüfungsorganisationssätze
Prüfungsnummer Semester Termin Prüfer/-in Abschluss
13103 20222 01 Remke, Anne (Prof. Dr.) (603602) E3 079 19
2014001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 105 13
31002 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 20
29001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 20
14101 20222 01 Remke, Anne (Prof. Dr.) (603602) E3 079 19
16010 20222 01 Remke, Anne (Prof. Dr.) (603602) L2 079 11
31001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 20
18001 20222 01 Remke, Anne (Prof. Dr.) (603602) 82 079 11
30001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 20
437001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 F23 20
16001 20222 01 Remke, Anne (Prof. Dr.) (603602) L2 079 11
438002 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 F23 20
30002 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 20
2015001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 105 13
29002 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 20
28001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 14
13104 20222 01 Remke, Anne (Prof. Dr.) (603602) E3 079 19
27001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 14
2013001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 105 13
438001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 F23 20
436002 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 F23 20
436001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 F23 20
13101 20222 01 Remke, Anne (Prof. Dr.) (603602) E3 079 19
14102 20222 01 Remke, Anne (Prof. Dr.) (603602) E3 079 19
29001 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 079 14
437002 20222 01 Remke, Anne (Prof. Dr.) (603602) 88 F23 20
13102 20222 01 Remke, Anne (Prof. Dr.) (603602) E3 079 19
17001 20222 01 Remke, Anne (Prof. Dr.) (603602) 82 079 11
Zuordnung zu Einrichtungen
Fachbereich 10 Mathematik und Informatik
Inhalt
Kommentar

Quantitatives Model Checking zielt darauf ab, Eigenschaften von randomisierten Modellen und Algorithmen zu verifizieren. Wir betrachten verschiedene Modellformalismen, von einfachen Transitionssystemen über Markov Ketten zu Markov Entscheidungsprozessen. Zu jeder Modellklasse wird die entsprechende Logik  vorgestellt, mit Hilfe derer auch komplexere Eigenschaften ausgedrückt werden können. Weiterhin werden zu jeder Logik die entsprechenden Algorithmen zum  Model Checking vorgestellt, die es ermöglichen, Eigenschaften zu verifizieren.

Neben dem Verständnis und der "händischen" Anwendung dieser Algorithmen sollen die erworbenen Kentnisse auch an Hand von Praxisbeispielen im Model Checking Tool PRISM eingesetzt werden. Hier können dann automatisiert größere und zum Teil parametrisierte Modelle verifiziert werden. Anwendungsbeispiele umfassen verschiedene randomisierte Algorithmen, sowie dynamisches Power Management.

Diese Vorlesung soll einen Überblick über Formalismen vermitteln, die verwendet werden können, wenn quantitative Aspekte, wie Zeit, Wahrscheinlichkeiten und Ressourcen eine zentrale Rolle spielen. Beim quantitativen Model Checking werden Wahrscheinlichkeiten für bestimmte Systemzustände errechnet, die dann mit bestehenden Wahrscheinlichkeitsschranken verglichen werden. Die Verfahren eignen sich daher besonders für die Bewertung der Zuverlässigkeit von - unter anderem - Eingebetteten Systemen.

Bemerkung

 Der Einschreibeschlüssel für den Learnweb-Kurs lautet: QMC


Strukturbaum
Die Veranstaltung wurde 4 mal im Vorlesungsverzeichnis WiSe 2022/23 gefunden:
Vorlesungen  - - - 1
Wahlbereich  - - - 2