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.
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
Infos zu Modulinhalt anzeigen
5 Videos•Insgesamt 44 Minuten
Allgemeine Einführung•6 Minuten
Modellprüfung•9 Minuten
Berechnungsbaum Logik•11 Minuten
Logischer Algorithmus für Berechnungsbäume•11 Minuten
Beispiel für die Logik des Berechnungsbaums•8 Minuten
3 Aufgaben•Insgesamt 30 Minuten
Größe des Zustandsraums•10 Minuten
CTL-Äquivalenz•10 Minuten
CTL-Beispiel•10 Minuten
BDDs Teil 1
Modul 2•1 Stunde abzuschließen
Moduldetails
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.
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
Infos zu Modulinhalt anzeigen
4 Videos•Insgesamt 35 Minuten
BDD Beispiele•11 Minuten
BDD-Algorithmus•10 Minuten
BDD-Algorithmus 2•6 Minuten
Beispiel für einen BDD-Algorithmus•8 Minuten
3 Aufgaben•Insgesamt 70 Minuten
BDD Quiz 1•20 Minuten
BDD Quiz 2•20 Minuten
BDD-Algorithmus•30 Minuten
BDD-basierte symbolische Modellprüfung
Modul 4•9 Stunden abzuschließen
Moduldetails
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
Infos zu Modulinhalt anzeigen
4 Videos•Insgesamt 39 Minuten
BDD-Algorithmus CTL•10 Minuten
Ein Beispiel: Füchse und Kaninchen•9 Minuten
Deadlock-Überprüfung in einem Netzwerk•10 Minuten
Netzwerke, BMC, Schlussfolgerungen•10 Minuten
3 Lektüren•Insgesamt 90 Minuten
NuSMV als Ursache des Problems mit Füchsen und Kaninchen•10 Minuten
Einführung•10 Minuten
Erläuterung der Paketvermittlungsnetze und der Datei zur Beschreibung der Routing-Funktion•70 Minuten
3 Aufgaben•Insgesamt 420 Minuten
Problem 1: farbige Murmeln•60 Minuten
Problem 2: Gleiche Werte erreichen•120 Minuten
Problem 3: Deadlocks in paketvermittelnden Netzwerken•240 Minuten
Dozent
Lehrkraftbewertungen
Lehrkraftbewertungen
Wir haben alle Lernenden um Feedback zu unseren Dozenten gebeten, ausgehend von der Qualität ihres Unterrichtsstils.
28DIGITAL ist Europas digitaler Innovationsmotor, eine Multi-Stakeholder-Plattform, verwurzelt in europäischen Werten und offen für die Welt. Wir verwandeln Wissen in Innovation, skalieren Start-ups zu globalen Unternehmen und bauen die nächste Generation digitaler Talente auf, um eine faire, wettbewerbsfähige und menschenzentrierte digitale Zukunft zu gestalten.
wir arbeiten an der Schnittstelle von Wissenschaft, Wirtschaft und Gesellschaft und verwandeln bahnbrechende Erkenntnisse in den Bereichen KI, Cybersicherheit, Robotik und fortschrittliche Computertechnik in Lösungen, die digitale Technologieinnovationen fördern, den ökologischen Wandel beschleunigen und das Leben der Menschen verbessern. 28DIGITAL bietet Online- und Präsenzunterricht in den Bereichen Innovation und Unternehmertum an, um die Qualität zu verbessern, die Vielfalt zu erhöhen und die Verfügbarkeit von Spitzeninhalten von 20 führenden technischen Universitäten in ganz Europa zu erweitern. Die Universitäten bieten eine einzigartige Mischung aus technischen Spitzenleistungen, unternehmerischen Fähigkeiten und Denkweisen für Digitalingenieure und Unternehmer in allen Phasen ihrer Karriere. Die akademischen Partner unterstützen die kühne Vision von Coursera, jedem Menschen an jedem Ort die Möglichkeit zu geben, sein Leben zu transformieren, indem sie Zugang zu den besten Lernerfahrungen der Welt bieten. Das bedeutet, dass 28DIGITAL nach und nach Teile seiner unternehmerischen und akademischen Bildungsprogramme zur Verfügung stellt, um seine Exzellenz zu demonstrieren und sie einem viel breiteren Publikum zugänglich zu machen. 28DIGITALs Online-Bildungsportfolio kann in gemischten Bildungssettings, in Master- und Promotionsprogrammen und von Fachleuten zur Aktualisierung ihres Wissens genutzt werden
Wann werde ich Zugang zu den Vorlesungen und Aufgaben haben?
Um Zugang zu den Kursmaterialien und Aufgaben zu erhalten und um ein Zertifikat zu erwerben, müssen Sie die Zertifikatserfahrung erwerben, wenn Sie sich für einen Kurs anmelden. Sie können stattdessen eine kostenlose Testversion ausprobieren oder finanzielle Unterstützung beantragen. Der Kurs kann stattdessen die Option "Vollständiger Kurs, kein Zertifikat" anbieten. 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.
Was bekomme ich, wenn ich mich für diese Specialization einschreibe?
Wenn Sie sich für den Kurs einschreiben, erhalten Sie Zugang zu allen Kursen der Spezialisierung, und Sie erhalten ein Zertifikat, wenn Sie die Arbeit abgeschlossen haben. Ihr elektronisches Zertifikat wird Ihrer Seite "Leistungen" hinzugefügt - von dort aus können Sie Ihr Zertifikat ausdrucken oder Ihrem LinkedIn-Profil hinzufügen.
Ist finanzielle Hilfe verfügbar?
Ja. Für ausgewählte Lernprogramme können Sie finanzielle Unterstützung oder ein Stipendium beantragen, wenn Sie die Einschreibegebühr nicht aufbringen können. Wenn für das von Ihnen gewählte Lernprogramm eine finanzielle Unterstützung oder ein Stipendium verfügbar ist, finden Sie auf der Beschreibungsseite einen Link zur Beantragung.