Vorlesungsaufzeichnungen

Elektronik I

Elektronik II

Grundlagen der Digitaltechnik

Test und Verlässlichkeit

Cooperation Systems WS 20/21

Entwurf digitaler Schaltungen

Multiagentensysteme und Algorithmische Spieltheorie

Mensch-Maschine-Interaktion

* Grundlagen der menschlichen Informationsverarbeitung * Paradigmen der Mensch-Maschine-Interaktion und des Interaktionsdesigns * Benutzerschnittstellen im Prozess des Software Engineerings * Ergonomiestandards * Evaluationsmethoden für interaktive Systeme * Kognitive und sozio-organisatorische Modelle * Methoden zur Dialog- und Aufgabenmodellierung * Fallstudien zu Interaktiven Systemen und Mensch-Maschine-Schnittstellen

Serious Games

Wissenschaftliche Arbeitstechniken für Seminare

Logik und Verifikation

This course is about logic based formal methods and how to use them for verification in computer science. It rigorously defines the language and semantics of sentential logic (SL) and first-order logic (FOL). We introduce the notion of a model, and show how hardware and software systems can be modelled within this framework. We also consider semantic entailment vs. syntactic derivability of formulae and how these two notions are related through correctness and completeness. Completeness is formally proved for SL and extensively discussed for FOL (in the form of refutation completeness). Both logics are applied to important verification problems: SL and its extension LTL for verifying linear temporal properties in concurrent systems, and FOL for verifying input/output properties of programs (the Hoare calculus). We show how the resolution calculus for FOL leads to PROLOG, a programming language based on FOL. We also show that SL leads to a declarative version of PROLOG: Answer Set Programming (ASP), that can be used to solve problems expressible on the second level of the polynomial hierarchy. While ASP is not a full-fledged programming language, it can be used for many naturally ocurring problems and it allows to model them in a purely declarative way. 1. Introduction 2. Sentential Logic (SL) 3. Verification I: Reactive Systems 4. First-Order Logic (FOL) 5. Verification II: Hoare Calculus 6. From FOL to PROLOG 7. PROLOG

Rechnernetze I

· Bitübertragungsschicht · Echtzeitzugang zu Rechnernetzen · Echtzeitübertragung in Netzen · xDSL (digital subscriber line) · Lokale Netze · SONET/SDH, Weitverkehrsnetze · Wegewahl in Weitverkehrsnetzen · Internet Protocol IP · Transportschicht, ISO-Transportdienst · Internet Protocol TCP · Breitband-ISDN, Asynchronous Transfer Mode (ATM)

Rechnernetze II

Teil 1: ISO-Darstellungsschicht (Schicht 6) · Kompression von Graphik/Bild/Video-Daten · Gliederung der Kodierungen · RLE, Huffman-Kode, Lempel-Ziv-Kode, Arithmetische Kodierung · JPEG, MPEG Teil 2: ISO-Anwendungsschicht (Schicht 7) Teil 2a: Internet-Dienste · Domain Name System (DNS) und Namensauflösung · Telnet, FTP, Email, USENET, World Wide Web · Client Server-Architekturen · Client-Server-Betriebsweise · HTTP-Protokoll · Web Browser Teil 2b: Internet-Anwendungen · NFS, CGI, Remote Procedure Calls · SUN RPCs · DCE, CORBA, (D)COM Middleware

Rechnerorganisation I

Die Vorlesung besteht aus den drei Teilen A, B und C. In Teil A sollen die Studierenden die Grundlagen der Rechnerarchitektur kennenlernen. In Teil B ist das Lernziel die Peripherieeinheiten eines Prozessors. In Teil C lernen die Studierenden die Architektur von RISC-Rechnern mit Schwerpunkt auf Verfahren zur Beschleunigung der Befehlsausführung.

Rechnerorganisation II

Teil 1: Vertiefung RISC-Rechner Teil 2: Parallelrechner

Werkzeuge der Informatik

· Einführung in die Skriptprogrammierung unter Unix/Linux · Wissenschaftlicher Textsatz mit Latex · Grundlagen und Werkzeuge des WWW · Datenrepräsentation mit XML · Wissenschaftliches Rechnen mit Matlab · Tabellenkalkulation und Präsentation

Komplexitätstheorie

The first chapter covers some topics from the Chomsky hierarchy: the Myhill-Nerode theorem (how to construct a minimal finite automaton), deterministic PDA’s, type 1 languages, normalform for type 0 and type 1 languages, Ehrenfeuchts theorem and Lindenmayer systems, a class of grammars that is orthogonal to parts of the Chomsky hierarchy. Chapter 2 discusses undecidability results in greater depth (Posts Correspondence theorem, (primitive) recursive functions, Hilberts 10. problem (solving diophantine equations)). We also cover Rices theorem and its analogue for grammars. Makanins problem (word equations over a free monoid) is decidable but not primitive recursive. Chapters 3 and 4 cover classical complexity results: time versus space, speed-up, gap-theorem, union-theorem and complexity classes: PH (the polynomial hierarchy), PSPACE, EXPSPACE and most of their interesting subclasses. We also cover closure properties and the Immerman/Szelepcsényi theorem. Chapter 5 covers the arithmetical and analytical hierarchy (extending EXPSPACE into the undecidable) and discusses descriptive complexity: can we find logics corresponding to complexity classes (Fagins theorem).

Informatik III

· Grammatiken der Chomsky Hierarchie (Typ3-Typ 0) · Reguäre Ausdrücke, Satz von Kleene, · Endliche Automaten (indet.), epsilon Kanten, Pumping Lemma, · Kellerautomaten, Turingmaschinen · Busy Beaver, Halteproblem, Reduktionen, aufzaehlbar/entscheidbar · Random access machines, P/NP

Künstliche Intelligenz

Die Aufzeichnungen wurden aus dem Sommersemester 2008 übernommen. Nur das Kapitel 5 wurde neu aufgezeichnet.