Niniejszy dokument stanowi kompleksowe studium teoretyczne mechanizmów dedukcyjnych zaimplementowanych w projekcie hats. Projekt ten bada ewolucję wiedzy w systemach wieloagentowych na grafach częściowej obserwacji, opierając się na Dynamicznej Logice Epistemicznej (DEL).
Podstawą symulacji jest modelowanie niepewności agentów za pomocą struktur Kripkego.
Globalny stan systemu (świat rzeczywisty) to wektor binarny
Topologia grafu
| Komponent Modelu | Matematyczna Definicja | Interpretacja Epistemiczna |
|---|---|---|
| Przestrzeń |
Zbiór wszystkich możliwych konfiguracji zabrudzeń/czapek. | |
| Zmienna |
Fakt "Agent |
|
| Relacja |
Kryterium nierozróżnialności dwóch światów przez agenta |
|
| Stan Epistemiczny |
Zbiór światów, które agent |
Ewolucja wiedzy następuje poprzez operatory ogłoszeń publicznych (Public Announcement Logic).
Początkowe ogłoszenie
Ważne założenie: Przyjmujemy, że rzeczywisty wektor stanu $\omega^$ nie jest wektorem zerowym ($\omega^ \neq \mathbf{0}$). W przeciwnym razie początkowe ogłoszenie publiczne
Niech
Twierdzenie: W grafie pełnym, jeśli obiektywnie istnieje
Szkic dowodu (Indukcja po
-
Baza (
$k=1$ ): Agent$i$ widzi same zera. $\mathcal{K}_i(0) = {\omega^, \mathbf{0}}$. Po $\phi_0$ zostaje tylko $\omega^$. Agent zgaduje w$t=0$ . -
Krok indukcyjny: Załóżmy, że dla
$k$ czapek agenci zgadują w$k-1$ . Przy$k+1$ czapkach, agent$i$ widzi$k$ czerwonych czapek. Gdyby sam miał białą, ktoś musiałby zgadnąć w$k-1$ . Milczenie w$k-1$ eliminuje światy z$k$ czapkami. Zostaje tylko świat z$k+1$ .
Twierdzenie: Prędkość propagacji informacji o braku wiedzy w grafie jest ograniczona przez odległość geodezyjną
Szkic dowodu: Redukcja
Twierdzenie: Jeśli centrum
Szkic dowodu: Liść
Problem sprawdzania wiedzy na grafach jest fundamentalnie trudny (Succinct Model Checking).
Problem weryfikacji wiedzy odpowiada ewaluacji zagnieżdżonych kwantyfikatorów, co plasuje go w klasie PSPACE-complete. Rozmiar modelu rośnie wykładniczo (
Aby sprostać wymaganiom wydajnościowym (bliskim standardom High-Frequency Trading), projekt wykorzystuje zaawansowane techniki przetwarzania równoległego:
-
Wektoryzacja SIMD: Operacje na zbiorach światów (
intersect_with,count) są zaimplementowane z wykorzystaniem instrukcji procesora (AVX2 / AVX-512). Dzięki zastosowaniu rejestrów takich jak__m256ii instrukcji typu_mm256_and_si256, możliwe jest przetwarzanie 256 bitów w jednym cyklu zegara. -
Złożoność: Dzięki wektoryzacji, bazowa złożoność operacji na zbiorze światów zostaje zredukowana z
$O(2^N)$ do$O(2^N / 256)$ , co pozwala na symulację systemów do$N=20$ w czasie rzeczywistym. -
Cache Locality: Struktura
WorldSetgwarantuje zwartość danych w pamięci, co minimalizuje kosztowne chybienia pamięci podręcznej (cache misses).
Symulacja potwierdza, że w systemach rozproszonych topologia jest epistemologią.
-
Gęstość krawędzi: W grafach gęstych (
$K_N$ ) wiedza powszechna buduje się przez zliczanie rund. -
Dystans fizyczny: W grafach rzadkich (
$C_N$ ) czas jest zdominowany przez geometrię sieci. -
Asymetria ról i Pasożytnictwo Informacyjne: W grafach asymetrycznych (jak
$S_N$ ) występuje zjawisko pasożytnictwa informacyjnego. Centrum grafu błyskawicznie buduje swoją wiedzę kosztem milczenia liści, jednak samo nie jest w stanie wygenerować milczenia, które zwrotnie pomogłoby liściom. Brak krawędzi między liśćmi o tym samym poziomie wiedzy prowadzi do trwałej pułapki informacyjnej.
mkdir build && cd build
cmake ..
make./test_graph- Graph representation using bitmasks (up to 64 vertices).
- Zero-allocation hot paths.
- C++17.