LTL su tracce finite per la verifica e la sintesi automatica di sistemi

This thesis aims to present an introduction to the problem of system synthesis from formulas. The work analyzes the foundations of , , finite-state automata and the techniques for translating to DFA, as well as presenting the main implementation approaches.

Questa tesi mira a presentare un’introduzione al problema della sintesi di sitemi a par- tire da formule . Il lavoro analizza i fondamenti di , , gli automi a stati finiti e le tecniche di traduzione da a DFA, oltre a presentare i principali approcci implementativi.