Logische Analyse und formale Verifikation von offenen, interaktiven Multiagentensystemen

Interaktive Systeme sind Informationsverarbeitende Systeme, die zwei oder mehr relativ autonome Agenten involvieren, welche miteinander interagieren müssen, um ihre Ziele zu erreichen (z.B. in Rechnernetzen, Produktionsstra?en, Handelsb?rsen usw.). Als wichtigstes Beispiel sind hier offene Systeme zu nennen, die dazu konstruiert werden, mit einer Umgebung zusammenzuarbeiten, welche im Voraus nicht oder nur teilweise bekannt ist oder sogar teilweise kontr?re Ziele verfolgt. Obwohl solche Systeme von enormer praktischer Relevanz sind, ist ihr Entwurf und der Nachweis der korrekten Funktionalit?t meist recht aufw?ndig, da die verfügbaren wissenschaftlichen Methoden nicht genügend ausgereift sind. In diesem Projekt geht es darum, formale logische Methoden und Werkzeugrahmen zu entwickeln, mit denen Wissen, Kommunikation, Ziele, Handlungen sowie Strategien von Agenten und Koalitionen in interaktiven Multiagentensystemen formalisiert werden k?nnen, und um die formale Spezifikation und Verifikation von Eigenschaften solcher Systeme. Diese grundlagenorientierten Forschungsarbeiten bilden die Basis neuer Programmierparadigmen für die n?chste Generation ubiquit?rer, intelligenter Ger?te.