A Forward-Only Construction of Semilinear Inductive Invariants for VAS

Sintesi Tecnica: Una Costruzione Solo-Avanti di Invarianti Induttivi Semilineari per i VAS

Enunciato del Problema
Il problema della raggiungibilità per i Sistemi di Addizione di Vettori (VAS), noti anche come reti di Petri, è un problema decisionale centrale nella teoria dei sistemi a stato infinito. Sebbene la decidibilità sia stata stabilita negli anni '80 da Kosaraju e Mayr, la complessità computazionale è rimasta aperta per decenni fino a tempi recenti, quando è stata dimostrata essere Ackermann-completa. Un approccio alternativo significativo alla decidibilità, introdotto da Leroux, caratterizza la non-raggiungibilità tramite invarianti induttivi semilineari. Questo metodo si basa su uno schema "avanti-indietro" (back-and-forth) che espande simultaneamente una sovra-approssimazione in avanti dal sorgente e una sovra-approssimazione all'indietro dal target.

Tuttavia, questo approccio esistente presenta due limitazioni primarie:

1. Dipendenza dalla Simmetria: La costruzione si basa sulla simmetria dei VAS, dove le esecuzioni possono essere invertite. Questa simmetria si rompe in modelli asimmetrici come i Branching VAS (BVAS), dove le esecuzioni sono a forma di albero anziché sequenze lineari, rendendo difficile l'estensione del metodo di Leroux ai BVAS.
2. Mancanza di Canonicità: Gli invarianti risultanti dipendono equamente sia dalla sorgente che dal target. In molti scenari di verifica, la sorgente è fissa mentre il target varia; un metodo che produce invarianti che cambiano drasticamente con il target è meno canonico e più difficile da relazionare con la struttura intrinseca del sistema. Inoltre, per sottoclassi specifiche come i VAS periodici, il metodo di Leroux non garantisce che gli invarianti risultanti siano periodici.

Metodologia
Gli autori propongono una nuova costruzione solo-avanti (forward-only) di invarianti induttivi semilineari. A differenza dell'approccio avanti-indietro, questo metodo costruisce invarianti esclusivamente a partire dall'insieme delle configurazioni iniziali ($C_0$), senza richiedere un ragionamento all'indietro dal target.

I componenti tecnici fondamentali includono:

• VAS Periodici: Gli autori definiscono una classe di VAS in cui l'insieme di raggiungibilità è periodico (chiuso rispetto all'addizione e contenente il vettore zero). Dimostrano che il problema della raggiungibilità per i VAS generali può essere ridotto al problema della raggiungibilità per i VAS periodici aggiungendo un singolo contatore.
• Insiemi Quasi Semilineari e Linearizzazione: Il metodo utilizza la caratterizzazione geometrica degli insiemi di raggiungibilità dei VAS come insiemi "quasi semilineari". Questi sono decomposti in insiemi "quasi lineari" ($b + P$), che vengono poi sovra-approssimati da insiemi lineari tramite un processo chiamato linearizzazione ($lin(L)$).
• Vettori Interni: Un concetto innovativo introdotto in questo lavoro è quello di "vettori interni" di un insieme periodico. Questi vettori permettono all'algoritmo di raffinare le approssimazioni spingendo i vettori all'interno dell'insieme originale, garantendo che l'invariante costruito rimanga disgiunto dall'insieme target pur mantenendo la periodicità.
• Costruzione Algoritmica: Il documento presenta un algoritmo (Algoritmo 1) che raffina iterativamente un insieme periodico semilineare $Inv$. In ogni iterazione, identifica la differenza tra la raggiungibilità in avanti dell'insieme corrente e l'insieme stesso, decompone questa differenza in componenti quasi lineari e aggiunge specifiche linearizzazioni traslate a $Inv$. Si dimostra che l'algoritmo termina perché la "dimensione spaziale" dell'insieme differenza diminuisce strettamente ad ogni iterazione.

Contributi Chiave

1. Costruzione Solo-Avanti: Gli autori introducono un metodo per costruire invarianti induttivi semilineari che dipendono principalmente dalle configurazioni raggiungibili dalla sorgente. Ciò produce invarianti che sono più canonici e meglio allineati con la struttura del sistema.
2. Invarianti Periodici per i VAS Periodici: Il documento prova che per i VAS periodici, se l'insieme di raggiungibilità è disgiunto da un insieme semilineare target, esiste un invariante induttivo semilineare periodico che è anch'esso disgiunto dal target. Questo contrasta con i metodi precedenti che potevano produrre invarianti non periodici anche per sistemi periodici.
3. Riduzione ai VAS Periodici: Gli autori forniscono una caratterizzazione efficace dei VAS periodici e dimostrano che il problema della raggiungibilità per i plain VAS si riduce a quello dei VAS periodici. Di conseguenza, gli invarianti semilineari per i VAS generali possono essere derivati dagli invarianti periodici costruiti per il sistema ridotto.
4. Prova di Esistenza tramite Oracle: La costruzione è presentata come un algoritmo con chiamate a oracle (per la linearizzazione e la selezione dei vettori). Il documento stabilisce l'esistenza dei vettori necessari e la terminazione del processo, fornendo una prova costruttiva dell'esistenza di invarianti induttivi semilineari periodici.

Risultati

• Teorema 4.5: L'insieme di raggiungibilità di un VAS periodico $(A, C_0)$ ha un'intersezione vuota con un insieme semilineare $C_{bad}$ se e solo se esiste un invariante induttivo semilineare periodico $I$ di $(A, C_0)$ tale che $I \cap C_{bad}$ sia vuoto.
• Terminazione e Correttezza: Il metodo proposto termina e restituisce un invariante induttivo semilineare periodico disgiunto dall'insieme target, a condizione che le chiamate all'oracle possano essere soddisfatte. La terminazione è garantita dalla stretta diminuzione della dimensione spaziale dell'insieme $Post^*_A(Inv) \setminus Inv$ ad ogni passo.
• Esempi: Il documento illustra il metodo con esempi in cui la costruzione solo-avanti produce invarianti che sono indipendenti dalla specifica configurazione target (a differenza del metodo avanti-indietro) e, nel caso dei VAS periodici, produce invarianti periodici laddove il metodo avanti-indietro fallisce nel farlo.

Significato e Rivendicazioni
Gli autori sostengono che questo approccio solo-avanti rappresenti un passo verso l'estensione delle tecniche basate su invarianti ai Branching VAS (BVAS). Poiché i BVAS mancano della simmetria necessaria per il ragionamento all'indietro (le configurazioni iniziali si trovano nelle foglie, i target alla radice degli alberi di esecuzione), il metodo avanti-indietro dipendente dalla simmetria è difficile da generalizzare. Costruendo invarianti puramente dalla sorgente, gli autori suggeriscono che il loro metodo sia più adatto ad affrontare il problema aperto della raggiungibilità per i BVAS.

Il documento discute inoltre la proprietà di "invariante induttivo semilineare" nel contesto dei Grammar VAS (GVAS), congetturando che proprietà simili possano valere, sebbene ciò rimanga un'area aperta per ricerche future. Il lavoro è inquadrato come un avanzamento teorico nella comprensione strutturale della raggiungibilità dei VAS, offrendo uno strumento più canonico per la verifica che rispetta l'asimmetria di certi modelli di sistema.