Model Checker LTL

Scopo del progetto è stata la realizzazione di un Model Checker che si occupasse della verifica di regole LTL su un modello dato in ingresso. Per fare questo è stata realizzata una libreria, quasi interamente scritta in Prolog, completa di tutte le funzioni necessarie per effettuare il checking.Inoltre viene fornito un manuale (in inglese) per aiutare nella comprensione del linguaggio che l'utente dovrà usare per sottoporre il codice delle proprie applicazioni al MC. Gli allegati sottostanti comprendono: un file jar in cui la libreria è stata aggiunta a quelle disponibili con il tool tuProlog per testare subito l'applicazione, i codici sorgenti, il file .class della libreria, il manuale utente,la relazione del progetto e inoltre un file pdf contenente i benchmark utilizzati durante lo sviluppo.