Tecniche di intelligenza artificiale basate su logica per la verifica di incompatibilità fra itinerari ferroviari

Lo scopo della tesi svolta in collaborazione con l’azienda Alstom riguarda il processo di sviluppo delle equazioni logiche che controllano i sistemi di interlocking delle stazioni. Tali sistemi sono già soggetti per normativa italiana ed europea a rigorosi controlli esaustivi della loro correttezza formale e fattuale. Tale fase di verifica comporta però elevati costi computazionali e temporali. Si è valutata perciò la possibilità di applicare metodi formali ai modelli di interlocking durante le prime fasi di sviluppo dei modelli stessi. Lo scopo specifico è quello di individuare possibili inconsistenze fin dai primissimi step di sviluppo, così da ridurre i tempi del processo di sviluppo stesso. In particolare, l’azienda ha fornito uno schema di esempio di una possibile stazione ferroviaria, ulteriormente semplificato ai fini di questo primo lavoro di analisi. L’azienda ha inoltre fornito uno schema di equazioni semplificate in cui sono state introdotte appositamente possibili incongruenze al fine di avere un caso di studio realistico. La direzione del lavoro esposto in questa tesi è quello relativo alla soluzione del problema della valutazione dell’incompatibilità di itinerari forroviari. La rete logica sequenziale che regola i sistemi di interlocking della stazione è modellata da numerose equazioni booleane e l’interfaccia utente è rappresentata da alcuni pulsanti la cui pressione provoca un cambiamento di stato nella rete. In particolare, tramite la pressione di appositi pulsanti è possibile comandare la registrazione degli itinerari della stazione. L’esito di tale registrazione è rappresentato dal valore logico di una particolare variabile propria per ciascun possibile itinerario. Il problema, nella sua prima formulazione, è quello di identificare le coppie di itinerari per cui il modello della rete logica impone un vincolo di mutua esclusività sulla registrazione.