An Intuitionistic Version of Computation Tree Logic

La mia tesi presenta una versione intuizionista della logica temporale CTL, conosciuta come Intuitionistic Computation Tree Logic (ICTL). Ho concentrato i miei sforzi nello sviluppo e nella comprensione di ICTL, che unisce la logica intuizionista e la Computation Tree Logic (CTL). Una caratteristica distintiva dell’ICTL sono i suoi modelli birelazionali e una sintassi che separa chiaramente le quantificazioni esistenziali e universali. Nella mia ricerca, ho delineato la sintassi e la semantica dell’ICTL, esaminato le proprietà dei modellibirelazionali e verificatolasoddisfacibilità delle formule dell’ICTL. Hoesplorato le differenze tra CTL e ICTL, in particolare la validità delle equivalenze dei punti fissi, introducendo una nuova versione di ICTL con una condizione aggiuntiva sui modelli per superare le limitazioni della proposta originale. Ho sviluppato un algoritmo efficiente di model checking per questa nuova versione di ICTL, evidenziando la sua complessità computazionale e le sue applicazioni pratiche nella verifica costruttiva delle proprietà dei sistemi. Nella mia tesi, ho enfatizzato l’importanza di ICTL nella verifica delle proprietà in vari contesti, inclusi i sistemi aperti, e ho evidenziato il suo potenziale per affrontare compiti di verifica più complessi rispetto alla classica CTL. Ho discusso l’applicazione dell’ICTL in diversi scenari, come il monitoraggio medico, la gestione dei database e il monitoraggio dei terreni agricoli, sottolineando la capacità di ICTL di garantire conoscenze persistenti e tracciabilità delle informazioni nel tempo. Infine, ho presentato un’estensione di VITAMIN, un prototipo progettato per la verifica formale dei Sistemi Multi-Agente (MAS), evidenziandone la modularità, la versatilità e la facilità di estensione per ospitare diverse logiche e modelli nella verifica delle proprietà. Ho fornito benchmark per dimostrare l’efficienza del processo di model checking ICTL in VITAMIN. Spero che la mia tesi possa contribuire alla letteratura esistente sulla CTL e stimolare ulteriori ricerche in questo campo.