AG 1, AG 2, AG 3   Info

AG Audience

-- Not specified --

Saarbrücken

In heutigen Verifikationswerkzeugen (FormalCheck, SMV, SPIN, etc.)
kommen unterschiedliche Spezifikationslogiken zum Einsatz, wie z.B.
lineare temporale Logik (LTL), "computation tree logic" (CTL) und der
modale mu-Kalkül. Nicht nur aus theoretischer Sicht, sondern auch aus
Sicht der Entwickler und Benutzer solcher Werkzeuge drängen sich damit
eine Reihe von Fragen auf, die die Ausdrucksstärke der verwendeten
Logiken betreffen. Im Vortrag sollen nach einer kurzen Einführung
zentrale Fragen vorgestellt und neuere Ergebnisse erläutert sowie
fundamentale Zusammenhänge mit der Theorie endlicher Automaten und
Halbgruppen aufgezeigt werden.

--email hidden

passcode not visible

logged in users only