Projection in a probabilistic epistemic logic and its application to belief-based program verification

Liu, Daxin; Lakemeyer, Gerhard (Thesis advisor); Belle, Vaishak (Thesis advisor)

Aachen : RWTH Aachen University (2022, 2023)
Doktorarbeit

Dissertation, RWTH Aachen University, 2022

Kurzfassung

Detaillierte Repräsentationen von Wissen und Aktionen sind ein Ziel, welches viele Wissenschaftler im Bereich der KI verfolgen. Unter den entwickelten Ansätzen ist das Situationskalkül von Reiter der wahrscheinlich am weitesten verbreitete. Es werden Aktionen als logische Terme dargestellt und Wissen durch logische Formeln kodiert. Die so entstandene Sprache wurde erweitert durch Features wie die Darstellung von Zeit, parallele Aktionen oder prozedurale Programmiersprachen. Zuletzt haben Belle und Lakemeyer eine modal Logik DS entwickelt, welche Glaubenssätze (sogenannte Beliefs) und Sensorrauschen formalisiert, durch die Modifizierung von Syntax und Semantik des Situationskalküls. Diese Logik hat bereits einige nützliche Eigenschaften, wie zum Beispiel vollständige Introspektion, aber es gibt auch noch Verbesserungspotenzial. Besonders problematisch ist die Quantifizierung des Glaubens (Degree of Belief). Derzeit kann der Degree of Belief nur durch Konstanten angegeben werden und eine exakte Darstellung durch Wahrscheinlichkeitsverteilungen ist nicht möglich. Außerdem fehlt ein Mechanismus um logische Schlüsse über Projektionen in die Zukunft zu formalisieren, also zu bestimmen, ob eine Anfrage über die Zukunft notwendigerweise aus der initialen Wissensbasis folgt. Im Allgemeinen existieren zwei Lösungsansätze für das Projektionsproblem, Regression und Progression. Während man bei Regression die Anfrage über die Zukunft in eine Anfrage über den initialen Wissensstand transformiert und dann evaluiert, projiziert man bei Progression die gesamte Wissensbasis in die Zukunft um die Anfrage direkt zu beantworten. In dieser Dissertation wird zunächst die Ausdrucksstärke der Logik DS erweitert durch Modifikation von Syntax und Semantik. Dann wird das Projektionsproblem untersucht. Es wird ein Regressionsoperator entwickelt, welcher Anfragen mit verschachtelte Beliefs und Quantoren in Belief Formeln unterstützt. Über die Progression wird gezeigt, dass diese mit der herkömmlichen Definition für ein Fragment der Sprache in Prädikatenlogik definierbar ist. Außerdem wird eine Lösung für Progression vorgestellt, welche den bezüglich Belief abgeschlossenen Teil der Wissensbasis nach der Ausführung von Aktionen betrachtet (only-believing). Die entwickelten Methoden werden in einem praktischen Szenario angewandt, bei der Verifizierung von Belief Programmen. Dies sind probabilistische Erweiterungen von Golog Programmen, wo jede Aktion und jede Wahrnehmung von Rauschen behaftet ist und Aussagen subjektiv durch den Belief des handelnden Agenten zu interpretieren sind. Es wird gezeigt, dass das Verifizierungsproblem untentscheidbar ist, sogar in stark eingeschränkten Szenarien. Außerdem wird ein Spezialfall des Problems vorgestellt, welches entscheidbar ist.