Metodi formali nello sviluppo software
a.a.2013/2014
Prof.Anna Labella
12/18/2015
1
Ripartiamo dagli automi
Stati e transizioni etichettate
 Gli automi sono caratterizzati dal
linguaggio che “accettano”

12/18/2015
2
L’algebra dei linguaggi
• Algebra di Boole
• Monoide rispetto alla concatenazione
• Iterazione
12/18/2015
3
L’algebra dei linguaggi
12/18/2015
4
L’algebra dei linguaggi
12/18/2015
5
12/18/2015
6
Equivalenza di automi
Accettare lo “stesso” linguaggio
– Il linguaggio di uno può ridursi al linguaggio
dell’altro usando le proprietà algebriche di P(A*)
12/18/2015
7
Sistemi reattivi
Protocolli di comunicazione
 Sistemi operativi
 Dispositivi di comando e controllo

12/18/2015
8

Sincronia ed asincronia

Comunicazione

Osservabilità

Non determinismo
12/18/2015
9
Sistemi di transizione
Sistemi stato-transizione: una macchina
astratta per la computazione
 Definizione
 Etichettatura
 Relazione con gli automi

12/18/2015
10

Sistema di transizione (etichettato) TS=(,S, ,
S0), dove
–
–
–
–
 è un alfabeto finito non vuoto
S è un insieme (finito) non vuoto di stati
 S  S è la relazione di trsansizione,
S0 S è l‘insieme degli stati inziali

simile ad un automa finito nondeterministico,
con molti stati iniziali ma senza stati finali

simile ad un modello di Kripke etichettato: un
sistema di mondi possibili con una nozione di
accessibilità
12/18/2015
11



Un sistema di transizione genera parole (finite o
infinite) w0w1w2... sse ci sono stati s0s1s2s3...
t.c. s0  S0 e (si,wi,si+1)  
Uno stato è identificato con le possibilità che mette
a disposizione
Problemi con la terminazione ed il deadlock
12/18/2015
12
Esempio: un registratore
off
dn
tape
1.
2.
3.
4.
up
dn
up
up
dn
memory
dn
play
={up, dn}
S={off, tape, memory, play}
={(off,dn,tape), (tape,up,off), (tape,dn,memory), (memory,up,off),
(memory,dn,play), (play,dn,tape), (play,up,off)}
S0={off}
12/18/2015
13
Sistemi di Transizione paralleli

Parallel transition system T=(T1,…,Tn)
– each Ti is a transition system
– SiSj=

interleaving semantics
– on its private alphabet, each Ti can make an
independent move
– synchronization is via common events

example: power switch and camcorder mode
12/18/2015
14
Example
camera
switch
but_hi
dn
on
off
up
but_lo
dn,
pwr_res
on
dn
tape
up,
pwr_fail
dn
memory
dn
play
dn
T=(switch, camera)
 {pwr_fail, pwr_res} are private to camera
 synchronization alphabet {up,dn}
12/18/2015
how big is the state space?
15

The global transition system T associated
with a parallel transition system (T1,…,Tn) is
defined as T=(, S, , S0), where

– = i
– S= S1 … Sn
– S0 = S1,0 … Sn,0, and
– ((s1,…,sn),a,(s1‘,…,sn‘)) iff for all Ti
• if ai, then ((s i),a,(s i‘))i, and
• if ai, then s i=s i‘.
12/18/2015
16
Finite State Automata
1kr

1kr
Coffee machine A1:
tea
coffee

Coffee machine A2:
1kr
1kr
1kr
tea
coffee

Are the two machines ”the same”?
12/18/2015
17