Metodi Di Verifica Di Sistemi 2025/2026

Rappresentazione dei sistemi mediante automi a stati finiti.
Rappresentazione della scomposizione di un sistema in sottosistemi mediante prodotto di automi, con varie tecniche di sincronizzazione.
Proprietà atomiche direttamente osservabili in ogni stato dell'automa.
Logica temporale: operatori temporali.
Logica temporale: quantificatori di cammino.
La Computational Tree Logic (CTL*), la complessità del problema della verifica di una proprietà di CTL*.
la logica CTL ottenuta restringendo in CTL* l'uso degli operatori temporali.
la logica PLTL (Propositional Linear Temporal Logic) ottenuta restringendo in CTL* l'uso dei quantificatori di cammino.
Algoritmo di tipo esplicito per la verifica di CTL.
Algoritmo di tipo esplicito per la verifica di PLTL.
Model Checking Simbolico:
algoritmo per la computatione simbolica di insiemi di stati
Il formalismo simbolico dei Binary Decision Diagrams (BDD)
Rappresentazione dei sistemi mediante BDD.
Model Checking basato sui BDD.
Tlmed Automata.
Caratteristiche dei Tlmed Automata.
Networks di Tlmed Automata e tecniche di sincronizzazione.
Logica Temporale Timed (Timed Temporal Logic)
Il Model Checking Timed.

---

Fonte: GOMP