Concurrency Theory WS 2011/2012: ================================ Erforderliche Vorkenntnisse: ============================ Formale Grundlagen der Programmierung Lernziele/Kompetenzen: ====================== Die Studierenden entwickeln operationelle Modelle für Systeme aus interagierenden Komponenten. Sie kennen verschiedene Korrektheitsbegriffe und verstehen die zugehörigen Verifikationsalgorithmen. Sie sind in der Lage, analoge Verfahren für verwandte Systemmodelle zu entwerfen. SWS, LP: ======== Vorlesung (4V+2Ü), 8 LP Sprache: ======== Deutsch (bei Bedarf Englisch) Anforderungsstufe: ================== Master (Anfänger) Vertiefung: =========== Entwicklung eingebetteter Systeme Verifikation Inhalt: ======= Multithreaded Programme und Petrinetze Petrinetz-spezifische Analysen Karp & Miller Überdeckungsgraphen Invarianten Unfoldings + SAT Statische Netzwerke und Lossy-Channel-Systems (LCS) Analyse wohlstrukturierter Transitionssysteme anhand von LCS WSTS und Finkels Finite-Reachability-Tree Abdullas Backwards-Algorithmus Geeraerts EEC-Algorithmus Dynamische Netzwerke und Prozessalgebren Analysierbarkeit Strukturelle Stationarität, Tiefe und Breite Wohlstrukturiertheit bei beschränkter Tiefe Berechnungsvollständigkeit bei beschränkter Breite Alternativer Korrektheitsbegriff: Bisimulationsäquivalenz Analysen und Grenzen Fixpunkte im Endlichen Kommunikationsfreiheit und Primelemente im Unendlichen Unentscheidbarkeit nach Jancar Prüfungsleistungen (Abschluss): =============================== Mündliche oder schriftliche Abschlussprüfung Prüfungsleistungen (Zulassungsvoraussetzungen): =============================================== Lösung von Übungsaufgaben Medienformen: ============= Tafel Beamer Skript und Folien zum Download (als pdf) Literatur: ========== Wird in der Vorlesung bekannt gegeben