Seminaria ogólnoinstytutowe:

Systemy wieloagentowe definiowane są jako układy komunikujących się agentów o pewnej autonomii, możliwości obserwacji środowiska i zdolności do podejmowania decyzji. Ewolucja systemu jest efektem interakcji agentów i środowiska. Weryfikacja przebiegu działania systemu jest zadaniem trudnym, głównie ze względu na wielkość przestrzeni stanów, która potrafi rosnąć wykładniczo wraz z liczbą komponentów. Logika ATL (Alternating-time Temporal Logic) jest jednym z popularniejszych języków specyfikacji własności systemów wieloagentowych. W swojej podstawowej wersji logika ta nie uwzględnia jednak wielu aspektów, takich jak obecność upływu czasu, niepełna informacja o stanie systemu, itp.

W trakcie wystąpienia przedstawię rezultat najprostszego, jak się wydaje, podejścia do wprowadzenia czasu do formuł ATL. W tym celu bieżąca wartość stanu systemu zostaje rozszerzona o zapis zawierający wskazania globalnego zegara, przy czym upływ czasu może przyjmować tylko dyskretne wartości. Jak się okazuje, w przypadku gdy nie jest oczekiwana pełna punktualność (tzn. rozważane własności dotyczą np. osiągnięcia pewnej konfiguracji przed lub po upływie zadanego czasu, ale nie precyzyjnie w momencie gdy zegar wskaże określoną wartość), możliwe jest zastąpienie strategii opartych na obserwacji zegara przez oparte na zliczaniu liczby odwiedzin w lokacjach automatu opisującego ewolucję. Ten i kilka innych wyników przedstawię w trakcie wystąpienia opartego na artykule "Timed ATL: Forget Memory, Just Count" napisanym wspólnie z E. Andre, L. Petrucci, W. Jamrogą i W. Penczkiem.