10.04.2008

Złożoność obliczeniowa logiki TeamLog dla współpracujących agentów

Na seminarium przedstawione zostaną wyniki badania złożoności obliczeniowej problemu spełnialności formuł logiki TeamLog, przeznaczonej do specyfikacji współpracujących agentów typu BDI.
Stworzony przez Barbarę Dunin-Kęplicz i Rineke Verbrugge formalizm TeamLog służy do specyfikacji agentów o architekturze BDI. W pełnej postaci łączy on rozmaite logiki wielomodalne do modelowania indywidualnych i grupowych przekonań agentów, ich postaw motywacyjnych, tworzących bazę do potencjalnej współpracy, jak również logikę dynamiczną, do specyfikacji indywidualnych akcji i wspólnych planów agentów, a następnie ich efektów.
W pierwszej fazie badań oceniono złożoność obliczeniową logiki TeamLog i jej indywidualnego fragmentu TeamLogInd. W obu przypadkach problem spełnialności jest rozstrzygalny, ale nierozwiązywalny z praktycznego punktu widzenia. W przypadku logiki TeamLogInd jest PSPACE zupełny, dla logiki TeamLog jest EXPTIME zupełny.
W związku z koniecznością prowadzenia wnioskowań w TeamLog podjęto problem scharakteryzowania tych fragmentów języka logiki TeamLog, które miałyby praktycznie rozwiązywalny problem spełnialności. Zbadano efekt standardowych ograniczeń języka logik wielomodalnych, takich jak:

• ograniczanie przez stałą głębokości modalnej formuł,
• ograniczanie przez stałą liczby zmiennych zdaniowych,
• ograniczanie kontekstu modalnego formuł,