Costruzione di strumenti per sistemi concorrenti e distribuiti con la teoria

In questo lavoro viene descritto un sistema che permette di provare sia proprietà comportamentali che logiche di sistemi concorrenti specificati con algebre di processo e con una logica delle azioni chiamata ACTL. Il sistema è stato realizzato integrando due strumenti esistenti, AUTO e EMC. Il primo costruisce Sistemi di Transizione Etichettati con azioni, a partire da un termine dell'algebra di processo, il secondo verifica la validità di formule CTL su macchine a stati finiti (Strutture di Kripke). I due strumenti vengono integrati implementando due funzioni di traduzione; la prima trasforma formule ACTL in formule CTL, la seconda trasforma Sistemi di Transizione Etichettati in Strutture di Kripke. La correttezza dell'integrazione segue dal fatto che le funzioni di traduzione preservano la soddisfacibilità delle formule logiche.