Der Kurs Automated Reasoning: Symbolic Model Checking lernen Sie, wie die Eigenschaften von handelnden Systemen und Programmen automatisch überprüft werden können. Der Grundbegriff ist ein Übergangssystem: jedes System, das durch Zustände und Schritte beschrieben werden kann. Wir zeigen, wie in der CTL (Computation Tree Logic) Eigenschaften wie die Erreichbarkeit beschrieben werden können. Typischerweise kann ein Zustandsraum sehr groß sein. Eine Möglichkeit, damit umzugehen, ist die symbolische Modellprüfung: eine Methode, bei der Mengen von Zuständen symbolisch dargestellt werden. Ein fruchtbarer Weg dazu ist die Darstellung von Zustandsmengen durch BDDs (binäre Entscheidungsdiagramme). In diesem Kurs werden Definitionen und grundlegende Eigenschaften von BDDs vorgestellt sowie die Algorithmen zu ihrer Berechnung, die für die CTL-Modellprüfung benötigt werden.
Automatisiertes Reasoning: Symbolische Modellüberprüfung
Dozent: Hans Zantema
2.702 bereits angemeldet
Bei 
enthalten
(26 Bewertungen)
Empfohlene Erfahrung
Wichtige Details
Zu Ihrem LinkedIn-Profil hinzufügen
12 Aufgaben
Erfahren Sie, wie Mitarbeiter führender Unternehmen gefragte Kompetenzen erwerben.
Erwerben Sie ein Karrierezertifikat.
Fügen Sie diese Qualifikation zur Ihrem LinkedIn-Profil oder Ihrem Lebenslauf hinzu.
Teilen Sie es in den sozialen Medien und in Ihrer Leistungsbeurteilung.
In diesem Kurs gibt es 4 Module
Nach einer allgemeinen Einführung in den MOOC beginnt dieses Modul mit einer allgemeinen Beschreibung der Modellprüfung. Dann wird die Computation Tree Logic (CTL) vorgestellt: eine Sprache, in der Eigenschaften von Übergangssystemen beschrieben werden können. Der Algorithmus, mit dem geprüft werden kann, ob eine solche Eigenschaft zutrifft, wird in einer abstrakten Umgebung angegeben, wobei nicht angegeben wird, wie die Zustandsmengen dargestellt werden.
Das ist alles enthalten
5 Videos3 Aufgaben
In diesem Modul werden BDDs (binäre Entscheidungsdiagramme) als Entscheidungsbäume mit Teilung eingeführt. Sie stellen boolesche Funktionen dar. Es werden zusätzliche Anforderungen an Entscheidungsbäume und BDDs vorgestellt, aus denen auf die Einzigartigkeit der Darstellung geschlossen werden kann.
Das ist alles enthalten
4 Videos3 Aufgaben
Nach einigen Beispielen für BDD wird der Algorithmus zur Berechnung des ROBDD einer beliebigen Aussageformel vorgestellt und diskutiert.
Das ist alles enthalten
4 Videos3 Aufgaben
In diesem letzten Modul werden die Themen CTL-Modellprüfung und BDDs kombiniert: Es wird gezeigt, wie BDDs verwendet werden können, um Zustandsmengen so darzustellen, dass der abstrakte Algorithmus für die CTL-Modellprüfung verwendet werden kann und viel größere Zustandsräume behandelt werden können als bei der expliziten zustandsbasierten Modellprüfung. Es werden mehrere Beispiele vorgestellt.
Das ist alles enthalten
4 Videos3 Lektüren3 Aufgaben
Dozent
von
Empfohlen, wenn Sie sich für Softwareentwicklung interessieren
Warum entscheiden sich Menschen für Coursera für ihre Karriere?
Neue Karrieremöglichkeiten mit Coursera Plus
Unbegrenzter Zugang zu 10,000+ Weltklasse-Kursen, praktischen Projekten und berufsqualifizierenden Zertifikatsprogrammen - alles in Ihrem Abonnement enthalten
Bringen Sie Ihre Karriere mit einem Online-Abschluss voran.
Erwerben Sie einen Abschluss von erstklassigen Universitäten – 100 % online
Schließen Sie sich mehr als 3.400 Unternehmen in aller Welt an, die sich für Coursera for Business entschieden haben.
Schulen Sie Ihre Mitarbeiter*innen, um sich in der digitalen Wirtschaft zu behaupten.
Häufig gestellte Fragen
Der Zugang zu Vorlesungen und Aufgaben hängt von der Art Ihrer Einschreibung ab. Wenn Sie einen Kurs im Prüfungsmodus belegen, können Sie die meisten Kursmaterialien kostenlos einsehen. Um auf benotete Aufgaben zuzugreifen und ein Zertifikat zu erwerben, müssen Sie die Zertifikatserfahrung während oder nach Ihrer Prüfung erwerben. Wenn Sie die Prüfungsoption nicht sehen:
Der Kurs bietet möglicherweise keine Prüfungsoption. Sie können stattdessen eine kostenlose Testversion ausprobieren oder finanzielle Unterstützung beantragen.
Der Kurs bietet möglicherweise stattdessen die Option 'Vollständiger Kurs, kein Zertifikat'. Mit dieser Option können Sie alle Kursmaterialien einsehen, die erforderlichen Bewertungen abgeben und eine Abschlussnote erhalten. Dies bedeutet auch, dass Sie kein Zertifikat erwerben können.
Wenn Sie sich für den Kurs einschreiben, erhalten Sie Zugang zu allen Kursen der Specializations, und Sie erhalten ein Zertifikat, wenn Sie die Arbeit abgeschlossen haben. Ihr elektronisches Zertifikat wird Ihrer Erfolgsseite hinzugefügt - von dort aus können Sie Ihr Zertifikat ausdrucken oder zu Ihrem LinkedIn-Profil hinzufügen. Wenn Sie die Kursinhalte nur lesen und ansehen möchten, können Sie den Kurs kostenlos besuchen.
Wenn Sie ein Abonnement abgeschlossen haben, erhalten Sie eine kostenlose 7-tägige Testphase, in der Sie kostenlos kündigen können. Danach gewähren wir keine Rückerstattung, aber Sie können Ihr Abonnement jederzeit kündigen. Siehe unsere vollständigen Rückerstattungsbedingungen.