Domande d'esame VERIFICATO
Teoria 13 febbraio 2023
78 visualizzazioni
Nessun voto ancora
Stai vedendo l'anteprima delle prime pagine. Il file completo è gratis: registrati per leggerlo tutto.
Di cosa parla
- Definire una locazione ASM e un aggiornamento inconsistente, fornendo un esempio causato dal non determinismo.
- Modello ASM per il funzionamento di porte metropolitane: controller apre le porte all'arrivo del treno e le richiude dopo 1 minuto; se un passeggero entra durante l'inChiusura, le porte si riaprono. Proprietà di raggiungibilità, safety e liveness relative al modello; descrivere una proprietà di raggiungibilità condizionata con logica temporale.
- Formalizzare in logica CTL la proprietà: se x>y ed y viene incrementato, allora prima o poi valgono x>0 e y>0.
- Rappresentare stati e transizioni di un Automa di Kripke in ROBDD; esempio con figura e implementazione in NuSVM.
- Dare la semantica in logica CTL dell’operatore AF e verificare per quali stati s vale la proprietà ??????,??????|= AF(??????) utilizzando l'algorithm di model checking.
Questo appunto è gratis. Registrati in 30 secondi per leggere tutte le pagine e scaricarlo.