Model checking

Problema di decidere se un modello formale di sistema soddisfa una proprieta' logica. La domanda tipica e' $M,s \\models \\varphi$ oppure $M \\models \\varphi$.

DFA/NFA

Automi su parole finite. Gli NFA possono avere piu' mosse possibili, ma riconoscono gli stessi linguaggi dei DFA tramite subset construction.

Residuo di linguaggio

Dato un prefisso $u$, il residuo $u^{-1}L$ contiene i suffissi $v$ tali che $uv \\in L$. In L* le righe della tabella approssimano residui.

Fairness

Vincolo sui comportamenti infiniti che elimina esecuzioni irrealistiche. Justice richiede che cio' che resta abilitato accada; compassion lega infinite abilitazioni a infinite occorrenze.

Automa di Büchi

Automa su parole infinite che accetta se una computazione visita stati finali infinitamente spesso. Il punto non e' raggiungere una fine, ma vedere una condizione ricorrente.

S1S / WS1S / S2S

Logiche monadiche del secondo ordine per strutture lineari o ad albero. S1S descrive omega-parole, WS1S insiemi finiti, S2S alberi binari infiniti.

LTL / CTL / CTL*

LTL quantifica implicitamente su un cammino lineare; CTL combina quantificatori di cammino e operatori temporali; CTL* generalizza entrambe.

OBDD

Rappresentazione canonica e compatta di funzioni booleane fissato un ordine delle variabili. Serve al model checking simbolico per evitare di enumerare stati uno per uno.

BMC

Bounded Model Checking: cerca controesempi di lunghezza limitata codificando sistema, proprieta' negata e vincolo di cammino come formula SAT.

Gioco di parita'

Gioco infinito su grafo dove vince chi soddisfa una condizione sui colori visti infinitamente spesso. E' centrale nella sintesi e nella soluzione di giochi omega-regolari.

Mealy machine

Macchina finita che produce output in risposta a input. Nella sintesi rappresenta una strategia implementabile del controllore.

Strong-cyclic solution

Piano per domini non deterministici che consente cicli, ma garantisce raggiungimento del goal sotto ipotesi di fairness sugli esiti.