Buchi automi formale verifica del software

Question

Come sto studiando l'applicazione di Buchi automi formale verifica del software, mi interessa la complessità computazionale (o link a documenti) per gli algoritmi utilizzati per risolvere il problema, in pratica.

Permettetemi di ricordare l'intuito matematico dietro il controllo del modello utilizzando queste tecniche.Buchi automi sono automi associato a $\omega$-linguaggi regolari.Si può pensare di queste lingue come l'infinito versione dei linguaggi regolari (infinito, nel senso che operano su infinito di parole).Come linguaggi regolari, essi godono di chiusura immobili in composizione e intersezione.È anche ben noto che questi Automi sono "isomorfi" alla proposta di una logica chiamata S1S.Questa è la logica di Monadico Secondo Ordine Logico (cioèsi può avere la quantificazione di predicati della logica, ma gli elementi possono spazia su un insieme finito).S1S è il bello di essere decidable, cioèper ogni preposizione siamo in grado di dire se è vero o no.Per trovare se un S1S formula è soddisfacibile, siamo in grado di trovare se associato atomata è uno stato accettante.In Buchi automi questo è fatto trovare i cicli tra lo stato iniziale e finale di stato.

Per trovare un "bug" in un software procedere come questo:

• formalizziamo il nostro software $\mathbb{S}$ utilizzando un S1S logica (un monaidic secondo ordine logico).
• si formalizzano le proprietà di sicurezza di nostri software nella logica $\mathbb{P}$
• ora usiamo la vicinanza di proprietà di $\omega$-lingue, a cui è associata la automi sono equivalenti a S1S logica:costruiamo Buchi automi di $\overline{\mathbb{S}} \cap \mathbb{P}$

In questo modo, se il software non rispettare le proprietà di sicurezza, risultante automi avrà almeno uno stato accettante.In pratica, l'accettazione dello stato di Buchi automi possono essere trovati da trovare un ciclo nel grafico associato tra lo stato iniziale e qualsiasi stato finale.

Ho il sospetto che, in pratica, di un algoritmo per la ciclo di rilevamento non può essere utilizzato.Questo è a causa del vincolo che il ciclo dovrebbe passare dal solo stato iniziale e dovrebbe passare attraverso un accettando di stato, quindi la probabilità di trovare il ciclo è necessario potrebbe essere molto bassa.Comunque, il miglior algoritmo per il Ciclo di rilevamento è risolto con l' Algoritmo Di Johnson nel tempo $O((n + e)(c + 1))$ e spazio delimitato da $O(n + t)$).

In pratica, S1S decidibility utilizzando Buchi automi potrebbe essere meglio per essere risolto con s-t connettività.Per esempio, NetworkX risolve s-t connettività con questo algoritmo da Abdol-Hossein Esfahanian.

Ho capito bene?

Il grafico viene utilizzato l'algoritmo in pratica per risolvere S1S satisfiability utilizzando Buchi automi?

Ho trovato questo, ma si vede solo una migliore riduzione da S1S a Buchi, e non parlare di grafici.