CMSO-transducing tree-like graph decompositions

Enunciato del Problema
Il lavoro affronta il problema della trasduzione di decomposizioni di grafi di tipo albero a partire da grafi utilizzando la logica Monadica del Secondo Ordine (MSO). Nello specifico, si cerca di determinare se decomposizioni quali le decomposizioni modulari, le decomposizioni split e le decomposizioni bi-join possano essere generate tramite trasduzioni CMSO (MSO con predicati di conteggio modulo).

Un lavoro precedente di Courcelle ha stabilito che tali decomposizioni potevano essere trasdotte utilizzando MSO invariante rispetto all'ordine, una logica strettamente più espressiva della CMSO. La questione aperta centrale affrontata qui è se sia possibile eliminare la dipendenza da un ordine lineare dei vertici, permettendo a queste decomposizioni di essere definite puramente all'interno della CMSO. Ciò è significativo perché le trasduzioni CMSO preservano l'equivalenza tra riconoscibilità da parte di automi ad albero e definibilità in logica per classi di grafi a larghezza di clique limitata (o larghezza di rango).

Metodologia
Gli autori sviluppano un quadro basato sulle proprietà strutturali dei sistemi di insiemi e dei sistemi di bipartizioni. La metodologia procede in diverse fasi:

1. Sistemi di Insiemi Laminari e Alberi: La sfida tecnica centrale è la trasduzione dell'albero laminare di un sistema di insiemi (un albero che rappresenta una famiglia di insiemi non sovrapposti). Gli autori introducono una tecnica per rappresentare ogni nodo interno dell'albero laminare utilizzando una coppia di foglie del suo sottoalbero. Dimostrano che per qualsiasi albero laminare, l'insieme dei nodi interni può essere partizionato in quattro insiemi "sottili". Per ogni insieme sottile, esiste una "bi-colorazione" (una partizione delle foglie in due insiemi disgiunti di uguale dimensione) che identifica univocamente i nodi in quell'insieme.
2. Selezione dei Rappresentanti tramite C2MSO: Utilizzando la proprietà degli insiemi sottili, gli autori costruiscono una trasduzione non deterministica $C_2$MSO. Questa trasduzione indovina quattro bi-colorazioni e utilizza predicati di conteggio ($C_2$) per definire una formula che seleziona una foglia rappresentante unica per ogni nodo interno. Ciò permette la costruzione della struttura dell'albero laminare (specificamente la relazione di antenato) a partire dal sistema di insiemi.
3. Estensione ai Sistemi Debolmente-Partitivi e Debolmente-Bipartitivi: Gli autori generalizzano la costruzione dell'albero laminare ai sistemi di insiemi debolmente-partitivi (che includono i moduli dei grafi) e ai sistemi debolmente-bipartitivi di bipartizioni (che includono split e bi-join). Si basano su teoremi strutturali (di Courcelle, Montgolfier e Rao) che affermano che tali sistemi possono essere caratterizzati da un albero laminare dotato di etichette specifiche per i nodi (degeneri, primi, lineari) e ordini parziali sui figli.
4. Decomposizioni Arricchite: Una volta trasdotta la struttura dell'albero sottostante, gli autori utilizzano trasduzioni MSO deterministiche per aggiungere il necessario "arricchimento" (ad esempio, relazioni di adiacenza tra fratelli nell'albero) richiesto per ricostruire il grafo originale. Ciò include la definizione di "m-archi" per le decomposizioni modulari, "c-archi" e "t-archi" per le decomposizioni split, e "r-archi" per le decomposizioni bi-join.

Contributi e Risultati Chiave
Il lavoro fornisce i seguenti risultati principali, formalizzati come trasduzioni non deterministiche $C_2$MSO:

• Alberi Laminari: Una trasduzione che, dato un sistema di insiemi laminare, ne produce l'albero laminare (Teorema 3.1).
• Alberi Debolmente-Partitivi: Una trasduzione che, dato un sistema di insiemi debolmente-partitivo, ne produce il suo "albero debolmente-partitivo" canonico (un albero laminare con etichette e ordini parziali) (Teorema 4.3).
• Decomposizioni Modulari: Una trasduzione che, dato un grafo diretto, ne produce la decomposizione modulare arricchita (Teorema 4.6).
• Cotrees: Una trasduzione che, dato un cograph, ne produce il suo cotree (Corollario 4.9).
• Alberi Debolmente-Bipartitivi: Una trasduzione che, dato un sistema debolmente-bipartitivo di bipartizioni, ne produce il suo "albero debolmente-bipartitivo" canonico (Teorema 5.4).
• Decomposizioni Split: Una trasduzione che, dato un grafo diretto fortemente connesso, ne produce la decomposizione split arricchita (Teorema 5.9).
• Decomposizioni Bi-join: Una trasduzione che, dato un grafo non diretto connesso, ne produce il suo "grafo scheletro" (una struttura equivalente alla decomposizione bi-join dalla quale il grafo può essere ricostruito) (Teorema 5.13).

Significato e Affermazioni
Gli autori affermano che i loro risultati migliorano il lavoro precedente di Courcelle eliminando il requisito dell'invarianza rispetto all'ordine. Raggiungendo queste trasduzioni utilizzando solo $C_2$MSO (che è più debole dell'MSO invariante rispetto all'ordine), dimostrano che queste decomposizioni canoniche sono definibili senza assumere un ordine lineare sui vertici.

Il lavoro evidenzia una specifica conseguenza teorica: per le classi di grafi in cui i grafi "primi" (rispetto alle decomposizioni split o bi-join) hanno larghezza di rango limitata e soddisfano la proprietà per cui la riconoscibilità equivale alla definibilità CMSO, questa equivalenza si estende all'intera classe. Ciò permette di estendere risultati noti sull'equivalenza tra riconoscibilità e definibilità a classi di grafi più ampie, come i grafi distance-hereditary e i grafi $(gem, co\text{-}gem)$-free, che precedentemente non si sapeva soddisfacessero questa proprietà sotto la sola CMSO.

Gli autori notano inoltre che i loro metodi sono sufficientemente generali da poter potenzialmente applicarsi ad altre strutture, come la decomposizione di Tutte dei matroidi o le decomposizioni modulari delle 2-strutture, sebbene queste non siano esplicitamente costruite nel lavoro. Infine, pongono la questione aperta se i predicati di conteggio ($C_2$) siano strettamente necessari per queste trasduzioni o se l'MSO standard sia sufficiente.