Automa regolare: la forma più nota di macchina Stato-Transizione a stati finiti.
Stati:
Transizioni:
Un automa regolare A è una tupla
, dove
Determinismo
L’automa è deterministico quando
Un comportamento (run) di A è una sequenza
dove .
Interpretazione: comportamento dell’automa a fronte di una sequenza di sollecitazioni dall’ambiente esterno.
Tradizionalmente un automa regolare viene proposto come macchina per il riconoscimento di linguaggi regolari, qui si enfatizza invece la reattività all’ambiente.
Una parola è accettata dall’automa A se esiste un run
Il linguaggio accettato da A è l’insieme .
Semantica espressa in termini di LTS.
L’LTS per l’automa regolare A è il grafo etichettato su
Si osserva che vi è coincidenza tra LTS ed automa e che un run di A è un cammino nell’LTS a partire dallo stato iniziale.
Osservazione: Gli automi regolari sono un formalismo di specifica di basso livello che coincidono con la struttura semantica.
Interpretazione tradizionale: gli automi regolari sono accettori di linguaggi (finitari).
Il linguaggio accettato da un automa potrebbe essere già visto come la semantica dell’automa (visione tradizionale che astrae dai comportamenti oggetto di specifico interesse nella specifica).
Un automa è una macchina che reagisce agli stimoli di un ambiente esterno.
Caratteristiche e limiti.
Potere espressivo: I limiti espressivi sono strettamente legati alla finitezza dello stato e alla mancanza di strutture dati (su domini illimitati).
Non adeguati a rappresentare sistemi che richiedono un numero illimitato di stati:
Naturalezza espressiva: è formalismo di specifica di basso livello.
Non consente la rappresentazione esplicita di:
Proprietà di chiusura (rispetto all’accettazione di linguaggi).
Chiusura rispetto alle operazioni più comuni:
Decidilità e complesità.
Il problema della raggiungibilità di uno stato è risolubile in tempo lineare sulla taglia dell’automa (numero di nodi e archi).
Il problema del linguaggio vuoto (è possibile raggiungere uno stato finale?) è un caso particolare di raggiungibilità.
L’intersezione di è l’automa
con
L’automa intersezione è ottenuto mettendo in parallelo i due automi e sincronizzando la loro evoluzione:
Automi con -transizioni per esprimere operazioni non controllabili.
Automi sull’alfabeto
L’uso di transizioni interne etichettate da permette di desincronizzare le azioni dell’automa rispetto all’input esterno.
Una parola è accettata dall’automa se esiste un cammino dell’LTS dallo stato iniziale
e
In alcuni contesti gli automi con azioni interne permetto maggiore naturalezza espressiva:
È possibile desincronizzare l’azione interna dall’ambiente esterno.
Fig.3: Automa per il contatore con il registro di scorrimento. Le azioni di scorrimento sono interne. Incrementi e decrementi sono controllati dall'esterno.
L’azione interna permette di costruire facilmente l’automa per l’unione di due automi :
Con una azione interna, si sceglie non-deterministicamente di proseguire come .
L’operazione di unione può essere utile per lo sviluppo incrementale di funzionalità (non interagenti) di una specifica.
L’azione interna permette di costruire facilmente l’automa per la concatenazione di due automi :
Con una azione interna, si collega ogni stato finale di con lo stato iniziale di .
L’operazione di concatenazione è utile per comporre sequenzialmente due blocchi di specifica.
La possibilità di esprimere azioni interne non controllabili non aumenta il potere espressivo degli automi, aumenta soltanto la naturalezza espressiva.
Automa sull’alfabeto
Costruzione di un automa A’ equivalente ad A senza azioni interne .
Sia per
Automa sull’alfabeto
1. Introduzione ai metodi formali di specifica
2. Semantica dei formalismi di specifica
3. Astrazione e Bisimulazione debole
4. FSM: Macchine a Stati Finiti
5. FSM: Non-determinismo e succintezza
7. FSM e Parallelismo – seconda parte
8. FSM e Parallelismo – terza parte
9. Promela
10. Specifica e verifica in SPIN
11. Proprietà di liveness in SPIN
12. Specifica di proprietà in Logica Temporale Lineare
13. Comportamenti infiniti: Automi di Büchi
14. Model checking di LTL basato su automi
15. Specifica di sistemi real time: Automi Temporizzati
16. Proprietà degli Automi Temporizzati
17. Problemi di decisione negli Automi Temporizzati
18. Il sistema di verifica UPPAAL