The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete

Technische Samenvatting: De Vergelijkingstheorie van Relationele Kleene-algebra met Graph Loop is PSpace-volledig

Probleemstelling
Het artikel behandelt de computationele complexiteit van de vergelijkingstheorie voor Relationele Kleene-algebra (RKA) uitgebreid met de graph loop operator (aangeduid als $\cdot^\circlearrowleft$ of fixset). De graph loop operator beperkt een binaire relatie tot de identiteitsrelatie (d.w.z. $R^\circlearrowleft = R \cap \Delta_X$). Terwijl de vergelijkingstheorie van standaard RKA bekend staat als PSpace-volledig, en uitbreidingen met intersectie ExpSpace-volledig zijn, was de complexiteit van de RKA met de graph loop operator (loop-RKA) een openstaand probleem. Voorgaand werk stelde vast dat het probleem PSpace-hard is en in ExpTime zit, maar de exacte bovengrens was onbekend. Voorts was de complexiteit van de RKA met de domein operator ($\cdot^d$) eveneens een openstaand probleem, ondanks het gerelateerde feit dat de theorie van RKA met antidomein ($\cdot^a$) bekend staat als ExpTime-volledig.

Methodologie
Om deze complexiteitsvragen te beantwoorden, introduceert de auteur een nieuw automaatmodel genaamd loop-automata. Dit zijn niet-deterministische eindige automaten die zijn uitgebreid met een specifieke transitietype dat test of de huidige vertex in een graafstructuur een loop bezit (d.w.z. een zelf-lus/self-edge).

De kern van de technische aanpak omvat de volgende stappen:

1. Loop-Automata Constructie: De auteur demonstreert dat elke loop-RKA term kan worden getransformeerd naar een equivalente loop-automaat in lineaire tijd, als een uitbreiding van de McNaughton–Yamada–Thompson constructie.
2. Pathwidth en Decompositie: Door gebruik te maken van de "lineair begrensde pathwidth model eigenschap" (vastgesteld in eerder werk voor gerelateerde logica's), beperkt het artikel de zoekruimte voor tegenmodellen tot structuren met een pathwidth die lineair begrensd is door de grootte van de invoertermen. Paddecompositie van deze gebonden-breedte structuren worden behandeld als strings.
3. Reductie naar 2AFA: De auteur construeert een reductie van het taal-inclusieprobleem van loop-automata naar het taal-inclusieprobleem van 2-weg alternerende eindige string-automata (2AFAs). Dit wordt bereikt door de paddecompositie als strings te coderen en het gedrag van de loop-automaat (inclusief de loop-testende transities) binnen het 2AFA-framework te simuleren.
4. Binaire Codering: Om te garanderen dat de reductie binnen PSpace blijft, hanteert het artikel een binaire codering van de graafstructuren (bags in de paddecompositie). Dit voorkomt de exponentiële opleving in de alfabetgrootte die zou optreden als structuren als atomaire symbolen zouden worden behandeld, een cruciale verfijning ten opzichte van eerdere algoritmen voor RKA met intersectie.
5. Uitbreiding naar Aanvullende Operatoren: De automata-constructie wordt aangepast om aanvullende operatoren te verwerken: top ($\top$), tests (zoals in Kleene Algebra met Tests, KAT), converse, en nominalen. Voor elke uitbreiding worden specifieke restricties op de structuren (bijv. het partitioneren van de identiteit voor tests, het afdwingen van symmetrie voor converse) gecodeerd als reguliere talen die worden afgewezen door hulp-2AFAs.

Belangrijkste Bijdragen en Resultaten
Het artikel stelt de volgende hoofdresultaten vast:

• Stelling 1: De vergelijkingstheorie van loop-RKA is PSpace-volledig. Dit lost het openstaande probleem met betrekking tot de complexiteit van loop-RKA op, waarbij de kloof wordt gedicht tussen de eerder bekende PSpace-hard/ExpTime-grenzen.
• Stelling 2: De vergelijkingstheorie van loop-RKA, uitgebreid met top, tests, converse en nominalen, is eveneens PSpace-volledig.
• Corollary 3: Als directe toepassing is de vergelijkingstheorie van Relationele Kleene-algebra met Tests (RKAT), uitgebreid met de domein operator (en range), PSpace-volledig. Dit lost een specifiek openstaand probleem op (McLean [21, Probleem 7.3] en Sedlár [36, p. 16]) betreffende de complexiteit van RKAT met domein.

Het artikel merkt een significant onderscheid op: terwijl het toevoegen van antidomein aan RKA de complexiteit verhoogt naar ExpTime-volledig, behoudt het toevoegen van domein (dat met graph loop en top kan worden gecodeerd) de PSpace bovengrens.

Significantie
De auteur claimt significantie op drie primaire gebieden:

1. Complexiteitsresolutie: Het stelt de complexiteit van de vergelijkingstheorie voor loop-RKA en RKAT met domein definitief vast als PSpace-volledig. Dit contrasteert met de ExpTime-volledigheid van RKAT met antidomein en de ExpSpace-volledigheid van RKA met algemene intersectie.
2. Algoritmische Innovatie: De introductie van loop-automata biedt een nieuw semantisch instrument voor het redeneren over relationele structuren met loop-restricties. De reductie naar 2AFAs via paddecompositie biedt een verfijnde algoritmische aanpak die PSpace-grenzen bereikt waar eerdere methoden (zoals voor PCoR*) ExpSpace vereisten.
3. Logische Verbindingen: De resultaten verhelderen de relatie tussen loop-RKA en Propositional Dynamic Logic (PDL). Hoewel loop-PDL ExpTime-volledig is, is de vergelijkingstheorie van loop-RKA strikt eenvoudiger (PSpace-volledig), wat een divergentie in complexiteit tussen de logica en de algebraïsche tegenhanger benadrukt wanneer deze tot vergelijkingen wordt beperkt. Daarnaast bieden de resultaten een directe PSpace bovengrens voor de geldigheid van incorrectheidstriples die domein en range bevatten, welke relevant zijn voor incorrectheidslogica.

De auteur benadrukt dat de aanpak steunt op de lineair begrensde pathwidth model eigenschap en dat de binaire codering van structuren cruciaal is voor het handhaven van de PSpace bovengrens, met name wanneer de intersectiewijdte niet vaststaat. Het artikel concludeert door te vermelden dat de eindige axiomatiseerbaarheid van loop-RKA een open vraag blijft.