Markoffsche Transitionssysteme modellieren zustandsbasierte Systeme, bei denen der Zustandswechsel zufällig geschieht, aber nicht von der Vergangenheit abhängig ist. Solche Modelle sind in der Informatik dann von Interesse, wenn große Systeme mathematisch modelliert werden müssen, deren Komponenten nach Zufallsgesetzen arbeiten (z. B. Betriebssysteme, Warteschlangennetze). Sie sind in der Programmanalyse für große Systeme interessant, weil mit ihrer Hilfe Methoden des model checking verfügbar gemacht werden können. Die Vorlesung befaßt sich mit den mathematischen Grundlagen Markoffscher Transitionssysteme, wobei insbesondere koalgebraische Methoden verfügbar gemacht werden sollen. Zunächst wird ein Einblick in die Arbeitsweise stochastischer Relationen gegeben, fundamentale Begriffe wie Morphismen, Kongruenzen, Bisimulationen werden eingeführt, die Existenz von Semi-Pullbacks wird nachgewiesen. Dann wird gezeigt, wie sich einfache modale Logiken mit diesen Systemen interpretieren lassen, was zur Frage der logischen Aquivalenz Markoffscher Transitionssysteme führt; diese Aquivalenz wird analysiert und mit Verhaltensäquivalenz auf der einen, Bisimulationen auf der anderen Seite in Beziehung gesetzt. Die Veranstaltung soll als Spezialvorlesung in ein interessantes Grenzgebiet zwischen Mathematik und Informatik einführen; je nach Interesse, Vorkenntnissen und Bedürfnissen der Zuhörer kann sie auch als Seminar organisiert werden. Sie setzt Grundkenntnisse der Maßtheorie und der Universellen Algebra voraus (die freilich kurz eingeführt werden).

Literatur:

S. Burris and H. P. Sankappanavar. A Course in Universal Algebra. Springer-Verlag (The Millenium Edition), 1981.

E.-E. Doberkat. Stochastic Relations. Foundations for Markov Transition Systems. Chapman & Hall/CRC Press, Boca Raton, New York, 2007.

E.-E. Doberkat. Stochastic Coalgebraic Logic. Springer-Verlag, 2009.

J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comp. Sci., 249(1):3 - 80, 2000. Special issue on modern algebra and its applications.

siehe auch:

Forschungsseite des Lehrstuhls zu diesem Thema