The complexity of being monitorable

Sintesi Tecnica: La Complessità dell'Essere Monitorabile

Enunciato del Problema
La Verifica al Runtime (RV) si basa sulla sintesi di monitor per determinare se le esecuzioni di un sistema soddisfano o violano una specifica. Una sfida centrale è la monitorabilità: la proprietà per cui una specifica permette la sintesi di un monitor capace di raggiungere eventualmente un verdetto (soddisfazione o violazione) basandosi sulle osservazioni delle esecuzioni. Sebbene la monitorabilità sia spesso studiata sintatticamente per specifici linguaggi di specifica, Diekert e Leucker [DL14] hanno proposto un approccio semantico e topologico. In questo framework, i comportamenti del sistema sono punti in uno spazio topologico $X$, e le osservazioni sono insiemi aperti. Una proprietà (un sottoinsieme $A \subseteq X$) è monitorabile se, per ogni osservazione aperta non vuota $U$, è possibile rifinarla in un insieme aperto non vuoto $V \subseteq U$ che sia interamente contenuto in $A$ o interamente nel suo complemento.

Il documento affronta la complessità della teoria degli insiemi descrittiva della famiglia di insiemi monitorabili, denotata $M(X)$, vista come un sottoinsieme dell'insieme delle parti $\mathcal{P}(X)$. Nello specifico, gli autori investigano quanto sia difficile determinare se un arbitrario sottoinsieme di uno spazio numerabile $X$ sia monitorabile. Essi analizzano la posizione di $M(X)$ all'interno della gerarchia di Borel e della gerarchia proiettiva, a seconda delle proprietà topologiche di $X$.

Metodologia
Gli autori utilizzano strumenti della teoria degli insiemi descrittiva [Kec95] e della riducibilità di Wadge.

1. Configurazione Topologica: Identificano $\mathcal{P}(X)$ con lo spazio di Cantor $2^X$ (tramite funzioni caratteristiche) dotato della topologia prodotto. Poiché $X$ è numerabile, $\mathcal{P}(X)$ è uno spazio polacco.
2. Caratterizzazione della Monitorabilità: Utilizzano la caratterizzazione secondo cui un insieme $A$ è monitorabile se e solo se l'interno del suo confine è vuoto ($\text{Int}(\text{Fr}(A)) = \emptyset$). Ciò equivale a dire che $A$ non è né denso né codenso in alcun insieme aperto non vuoto.
3. Analisi della Complessità: Classificano $M(X)$ determinando se appartiene a specifiche classi di punti ($\Sigma^0_\alpha, \Pi^0_\alpha, \Sigma^1_1, \Pi^1_1$) e se è completa per tali classi. Ciò comporta la costruzione di riduzioni continue da insiemi noti per la loro durezza (ad esempio, insiemi $\Sigma^0_3$-completi o $\Pi^1_1$-completi) verso $M(X)$.
4. Distinzione dei Casi: L'analisi è divisa in due casi primari:
   • Spazi Second Countable: Dove $X$ possiede una base numerabile.
   • Spazi Non Second Countable: Dove $X$ è numerabile ma manca di una base numerabile.

Contributi Chiave e Risultati

1. Il Caso Second Countable
Per uno spazio topologico numerabile e second countable $X$, la famiglia $M(X)$ è sempre un sottoinsieme $\Pi^0_3$ di $\mathcal{P}(X)$. Il documento fornisce una classificazione precisa delle possibili complessità che $M(X)$ può raggiungere:

• $\Delta^0_1$ (Clopen): Si verifica se $M(X) = \mathcal{P}(X)$, il che accade se e solo se l'insieme dei punti isolati è denso in $X$.
• $\Sigma^0_2$-completo: Si verifica in spazi come la topologia cofinita su un insieme numerabile.
• $\Pi^0_3$-completo: Si verifica in spazi come la topologia di Alexandrov su $\mathbb{N}^2$ con un particolare ordine parziale.
• Risultati di Impossibilità: Gli autori dimostrano che per gli spazi second countable, $M(X)$ non può essere $\Sigma^0_1$-completo, $\Delta^0_2$-sharp o $\Pi^0_2$-completo.

Un criterio operativo cruciale viene derivato (Rimarca 3.15): $M(X)$ è $\Pi^0_3$-completo se e solo se, dopo aver rimosso l'unione di tutti gli insiemi aperti minimi non vuoti, l'interno rimanente contiene infiniti sottoinsiemi aperti disgiunti tra loro. Altrimenti, $M(X)$ è $\Sigma^0_2$.

2. Applicazione alle Relazioni di Transizione
Gli autori applicano questi risultati alle topologie indotte da relazioni di transizione su un insieme numerabile di stati (modellando sistemi di tipo branching-time). Definiscono $R_0$ come l'insieme delle relazioni di transizione che inducono una famiglia di insiemi monitorabili $\Sigma^0_2$, e $R_1$ come quelle che inducono una famiglia $\Pi^0_3$-completa.

• Teorema 3.18: Sia $R_0$ che $R_1$ sono sottoinsiemi Borel dello spazio di tutte le relazioni di transizione. Inoltre, $R_0$ è comeatrico (residuo), il che significa che "la maggior parte" delle relazioni di transizione (nel senso della categoria di Baire) induce una famiglia di insiemi monitorabili topologicamente semplice ($\Sigma^0_2$).

3. Il Caso Non Second Countable
Il documento dimostra che la restrizione agli spazi second countable è essenziale.

• Esempio: Gli autori costruiscono uno spazio numerabile, non second countable (basato sulla topologia di Scott su sequenze finite con un elemento $\infty$).
• Risultato: Per questo spazio, la famiglia di insiemi monitorabili $M(X)$ è $\Pi^1_1$-completa (completa coanalitica). Questo rappresenta un salto significativo nella complessità rispetto al caso second countable, mostrando che senza la seconda numerabilità, il problema di determinare la monitorabilità può essere difficile quanto il problema della ben-fondatezza degli alberi.

Significato
Il lavoro fornisce un framework unificante e indipendente dalla sintassi per comprendere la monitorabilità. Mappando il problema nella teoria degli insiemi descrittiva, stabilisce che:

1. Nell'impostazione standard degli spazi second countable (che include molti modelli di verifica al runtime), la complessità della determinazione della monitorabilità è limitata all'interno della gerarchia di Borel, specificamente al livello $\Pi^0_3$.
2. Esiste un chiaro criterio strutturale (relativo agli insiemi aperti minimi e alla disgiunzione) che determina se un particolare modello di sistema produce un problema di monitorabilità "semplice" ($\Sigma^0_2$) o "complesso" ($\Pi^0_3$-completo).
3. L'assunzione di seconda numerabilità è critica; allentarla permette di raggiungere una complessità arbitrariamente alta (fino a $\Pi^1_1$-completa), evidenziando l'importanza dei vincoli topologici nell'analisi teorica della verifica al runtime.

Il lavoro non propone nuovi algoritmi per la sintesi di monitor, ma delinea i limiti teorici e le proprietà strutturali del problema decisionale della monitorabilità attraverso diversi modelli topologici.