Technische Samenvatting: De Complexiteit van het Definiëren en Scheiden van Fixpuntformules in Modale Logica

1. Probleemstelling

Het artikel onderzoekt het probleem van de modale scheidbaarheid (modal separability) van de modale $\mu$-calculus ($\mu$ML) met betrekking tot propositionele modale logica (ML). Gegeven twee inconsistente $\mu$ML-formules $\phi$ en $\phi'$, vraagt het probleem of er een ML-formule $\psi$ bestaat (een "separator") zodanig dat $\phi \models \psi$ en $\psi \models \neg \phi'$.

Dit probleem generaliseert modale definieerbaarheid: het bepalen of een specifieke $\mu$ML-formule equivalent is aan een ML-formule. Definieerbaarheid is het speciale geval waarbij $\phi' = \neg \phi$. De studie wordt uitgevoerd over diverse klassen van modellen die relevant zijn voor de informatica:

• Willekeurige modellen (onbeperkte uitgraad).
• Woorden (modellen met uitgraad $\le 1$, aangeduid als $T_1$).
• Binaire bomen (uitgraad $\le 2$, aangeduid als $T_2$).
• Bomen met een begrensde uitgraad $d \ge 3$ (aangeduid als $T_d$).
• Eindige modellen en oneindige woorden.

De auteurs onderzoeken ook het probleem van het bestaan van de Craig-interpolant (een speciaal geval van scheidbaarheid waarbij de separator alleen symbolen mag gebruiken die gemeenschappelijk zijn aan $\phi$ en $\phi'$) en de effectieve constructie van separators.

2. Methodologie

De auteurs maken gebruik van een combinatie van modeltheoretische karakteriseringen en automata-theoretische technieken:

• Modeltheoretische Karakteriseringen: De kern van de beslissingsprocedure berust op gezamenlijke consistentie (joint consistency). Twee formules zijn niet scheidbaar dan en slechts dan als ze "gezamenlijk consistent" zijn met betrekking tot specifieke bisimulatie-relaties. Specifiek: $\phi$ en $\phi'$ zijn niet ML-scheidbaar over een klasse $\mathcal{C}$ als ze gezamenlijk consistent zijn met betrekking tot $(\sigma, n)$-bisimulaties voor alle $n$.

  • Voor woorden ($T_1$) en binaire bomen ($T_2$) maken de auteurs gebruik van het feit dat bisimilariteit impliceert dat er sprake is van isomorfie (of dat dit tot isomorfie gereduceerd kan worden) om gezamenlijke bisimulatie-consistentie gelijk te stellen aan gezamenlijke isomorfie-consistentie.
  • Voor $d \ge 3$ faalt deze equivalentie, wat een complexere analyse vereist via bisimulatie-quotiënten.

• Automata Theorie: Het artikel maakt gebruik van de bekende correspondentie tussen $\mu$ML en Niet-deterministische Pariteitsboomautomata (NPTA).

  • $\mu$ML-formules worden vertaald naar NPTA's.
  • Het probleem van het controleren van gezamenlijke consistentie wordt gereduceerd tot het controleren van de intersectie van de talen geaccepteerd door deze automata.
  • Een cruciaal technisch instrument is de constructie van automata die bisimulatie-quotiënten herkennen van de talen geaccepteerd door de oorspronkelijke automata. Dit stelt de auteurs in staat om scheidbaarheid over bomen met een begrensde uitgraad te beslissen door het te reduceren tot de isomorfie-controle van deze quotiënten.

• Constructie van Separators: Wanneer scheidbaarheid is vastgesteld, bieden de auteurs algoritmen aan voor de constructie van de scheidende formule. Deze constructies omvatten vaak het genereren van ML-uniforme consequenties van de invoerformules, wat disjuncties zijn van types die consistent zijn met de input.

3. Belangrijkste Bijdragen en Resultaten

3.1. Complexiteit van Scheidbaarheid en Definieerbaarheid

Het artikel stelt een precieze complexiteitslandschap vast voor ML-scheidbaarheid en ML-definieerbaarheid van $\mu$ML-formules, samengevat in Tabel 1 van het artikel:

Modelklasse	ML-Definieerbaarheid	ML-Scheidbaarheid	Grootte van Separator-constructie
Woorden ($T_1$)	PSpace-compleet	PSpace-compleet	Enkelvoudig exponentieel
Binaire Bomen ($T_2$)	ExpTime-compleet	ExpTime-compleet	Dubbel exponentieel
Onbeperkte Modellen	ExpTime-compleet	ExpTime-compleet	Dubbel exponentieel
Bomen ($T_d, d \ge 3$)	ExpTime-compleet	2-ExpTime-compleet	Driedubbel exponentieel

• Woorden ($T_1$): Scheidbaarheid is PSpace-compleet. Dit is het eenvoudigste geval, wat overeenkomt met de complexiteit van $\mu$ML-verzadigbaarheid over woorden.
• Binaire Bomen ($T_2$) en Onbeperkt: Scheidbaarheid is ExpTime-compleet. De auteurs tonen aan dat de structurele eigenschappen van binaire bomen (waarbij bisimilariteit isomorfie impliceert) een gemeenschappelijke algoritmische behandeling mogelijk maken met onbeperkte modellen.
• Bomen met $d \ge 3$: Dit is de meest significante bevinding. Terwijl ML-definieerbaarheid ExpTime-compleet blijft, springt ML-scheidbaarheid naar 2-ExpTime-compleet.
  • De auteurs tonen aan dat deze toename in complexiteit niet louter komt door het coderen van hogere uitgraden in binaire bomen (wat de complexiteit zou behouden).
  • De hardheid ontstaat omdat ML niet beschikt over de Craig-interpolatie-eigenschap (CIP) over $T_d$ voor $d \ge 3$.

3.2. Craig-interpolatie en Bestaan van Interpolanten

• Falen van CIP: Het artikel bewijst dat ML de Craig-interpolatie-eigenschap bezit over alle modellen, woorden en binaire bomen, maar dat deze faalt over bomen met uitgraad $d \ge 3$.
• Bestaan van Interpolanten: Gemotiveerd door het falen van CIP, bestuderen de auteurs het probleem van het bestaan van de Craig-interpolant (bestaat er een separator die alleen gemeenschappelijke symbolen gebruikt?) voor ML over $T_d$ ($d \ge 3$). Zij tonen aan dat dit probleem coNExpTime-compleet is, wat strikt moeilijker is dan het geldigheidsprobleem voor ML (dat PSpace-compleet is over deze klassen).

3.3. Effectieve Constructie

Het artikel biedt algoritmen voor het construeren van separators wanneer deze bestaan:

• Woorden: Constructie is mogelijk in exponentiële tijd (optimaal, aangezien $\mu$ML exponentieel compacter is dan ML over woorden).
• Binair/Onbeperkt: Constructie is mogelijk in dubbel exponentiële tijd.
• $d \ge 3$: Constructie is mogelijk in driedubbel exponentiële tijd.
• De auteurs merken op dat voor $d \ge 3$ de geconstrueerde separators naar verwachting optimaal zijn in grootte, hoewel een formeel ondergrens voor de constructiegrootte nog openstaat.

3.4. Gegradeerde Modale Logica (Casestudy)

De auteurs breiden hun resultaten uit naar Gegradeerde Modale Logica (grML) en de Gegradeerde $\mu$-calculus (gr$\mu$ML), die modaliteiten bevatten die het aantal opvolgers tellen (bijv. "ten minste $k$ kinderen voldoen aan...").

• Met Grades in de Separator: Zowel definieerbaarheid als scheidbaarheid blijven ExpTime-compleet.
• Zonder Grades in de Separator:
  • Definieerbaarheid: ML-definieerbaarheid van gr$\mu$ML-formules is ExpTime-compleet.
  • Scheidbaarheid: ML-scheidbaarheid van gr$\mu$ML-formules is 2-ExpTime-compleet.
  • De auteurs schrijven de hogere complexiteit van scheidbaarheid (vergeleken met definieerbaarheid) toe aan het feit dat bomen met een begrensde ariteit definieerbaar zijn in gr$\mu$ML, waardoor de reductie van het algemene $d \ge 3$ geval naar de gegradeerde setting mogelijk is.

4. Betekenis en Claims

Het artikel claimt een "vrij volledig en interessant beeld" te geven van de complexiteit van definieerbaarheid en scheidbaarheid voor fixpuntlogica's. De primaire betekenis ligt in:

1. Identificatie van een Complexiteitsgat: Het is het eerste bekende geval in dit gebied van de logica waar scheidbaarheid bewezen moeilijker is dan definieerbaarheid (specifiek 2-ExpTime versus ExpTime) voor een natuurlijke logica over een standaard klasse van modellen. Dit contrasteert met eerdere resultaten waar scheidbaarheid ofwel gelijk aan, ofwel gemakkelijker dan definieerbaarheid was.
2. Verbinding van Interpolatie en Complexiteit: Het werk legt een directe link tussen het falen van de Craig-interpolatie-eigenschap en de verhoogde computationele complexiteit van het scheidbaarheidsprobleem. Het gebrek aan CIP over $d \ge 3$ bomen wordt aangetoond de wortel te zijn van de 2-ExpTime hardheid.
3. Verfijning van het Landschap van de Modale Logica: De resultaten verduidelijken dat de complexiteit van modaal redeneren niet uniform is over boomstructuren; de overgang van binaire naar ternaire bomen verandert de logische eigenschappen (specifiek interpolatie) en de computationele kosten van redeneertaken zoals scheidbaarheid fundamenteel.
4. Constructieve Resultaten: Naast beslissingsprocedures biedt het artikel effectieve constructies voor separators, waarbij grenzen worden gesteld aan de grootte van deze separators (bijv. dubbel exponentieel voor binaire bomen, driedubbel exponentieel voor $d \ge 3$).

De auteurs concluderen dat hun bevindingen de subtiele wisselwerking tussen de structurele eigenschappen van modellen (uitgraad), de logische eigenschappen van de taal (interpolatie) en de computationele complexiteit van redeneertaken benadrukken. Zij laten openstaande vragen over de optimaliteit van de grootte van de separators voor $d \ge 3$ en de uitbreiding van deze resultaten naar andere fragmenten of operatoren.