**UNIUD è ricerca**
STIMOLA CURIOSITA’, PASSIONE E CORAGGIO

Logiche, automi e verifica automatica

Cluster di dipartimento

Informatica teorica

Descrizione

I temi di ricerca di interesse per il gruppo spaziano su diversi fronti che possono essere così raggruppati:

Logiche temporali per l’informatica. Uso delle logiche temporali basate sui punti o sugli intervalli quali linguaggi per la specifica, la verifica automatica e la sintesi di sistemi complessi. Decidibilità e complessità dei problemi della soddisfacibilità, del model checking e della sintesi. Formalizzazione e risoluzione di problemi informatici (ad esempio, il problema della pianificazione automatica) attraverso sistemi di logica temporale.
Automi. Definizione e analisi di opportune classi di automi con contatori per esprimere proprietà non catturate dai linguaggi omega-regolari. Modellazione mediante automi ibridi di sistemi che coinvolgono componenti discrete e continue. Identificazione di classi decidibili di automi ibridi. Analisi di proprietà temporali su automi ibridi. Analisi di sistemi parametrici. Verifica di proprietà temporali di protocolli e algoritmi quantistici. Algoritmi di contrazione mediante simulazione/bisimulazione. Codifica numerica di automi.
Verifica di soddisfacibilità. Decidibilità e complessità computazionale del problema della soddisfacibilità per logiche temporali ad intervalli rispetto a diverse semantiche (con o senza intervalli puntuali, con l’assunzione o meno di omogeneità). Sviluppo e implementazione di sistemi a tableau per logiche temporali a intervalli. Sviluppo e implementazione di sistemi a tableau alternativi per la logica del tempo lineare (LTL) e per varie sue estensioni e confronto con procedure di decisione alternative (basate sugli automi, via risoluzione, mediante l’uso di algoritmi di model checking simbolico).
Verifica di equivalenza osservazionale. Bisimulazioni su Sistemi di Transizioni Etichettati (LTS), specialmente in riferimento ad aspetti di sicurezza, e relativi algoritmi di decisione. Bisimulazione per LTS con aspetti quantitativi e catene di Markov a tempo discreto e continuo. Algoritmi di lumping.
Model checking. Model checking per sistemi a stati finiti e sistemi a stati infiniti con logiche temporali ad intervalli rispetto a semantiche diverse. Confronto tra model checking di logiche temporali basate sui punti (LTL, CTL e CTL*) e model checking di logiche temporali ad intervalli.
Interpretazione astratta. Verifica mediante interpretazione astratta per sistemi reattivi. Sviluppo di strumenti per la verifica di proprietà espresse in LTL e sue estensioni. Studio di varianti dei sistemi a tableau per sistemi di vincoli che sono alla base del motore di verifica di tali strumenti. Verifica mediante interpretazione astratta per linguaggi funzionali e logico-funzionali. Sviluppo di strumenti per la verifica di proprietà delle risposte calcolate espresse in domini approssimati, sia tipici della letteratura in interpretazione astratta che sviluppati appositamente.
Sintesi. Studio del problema della sintesi per logiche ad intervalli, e per loro estensioni con una relazione di equivalenza, rispetto a ordinamenti lineari finiti e al dominio dei naturali. Caratterizzazione del problema mediante giochi logici.

Linee di ricerca

Studio sistematico del potere espressivo e della decidibilità/complessità computazionale delle logiche temporali ad intervalli rispetto ai problemi della verifica della soddisfacibilità e del model checking.
Confronto fra l’espressività delle logiche temporali ad intervalli e delle tradizionali logiche temporali basate sui punti (LTL, CTL, CTL* e loro varianti/estensioni).
Formalizzazione in logica temporale degli approcci al problema della pianificazione automatica proposti in letteratura (approcci basati su azioni e approcci basati su timeline) al fine di caratterizzare e confrontare il loro potere espressivo e la loro complessità.
Utilizzo delle logiche temporali ad intervalli per la pianificazione automatica al fine di gestire aspetti quali azioni con durata, accomplishment e aggregazioni temporali.
Caratterizzazione in termini di automi e logiche (classiche e temporali) delle diverse estensioni delle espressioni omega-regolari proposte in letteratura.
Studio della decidibilità e delle proprietà di chiusura delle classi di automi proposte.
Identificazione di classi di automi su cui è possibile definire algoritmi simbolici per il calcolo della raggiungibilità.
Definizione di semantiche approssimate che meglio riflettano i comportamenti reali dei sistemi modellati.
Modellazione di sistemi parametrici attraverso sistemi dinamici a tempo discreto polinomiali e parametrici la cui analisi può essere effettuata efficientemente attraverso i coefficienti di Bernstein
Definizione di una semantica basata su Quantum Markov Chain per circuiti e algoritmi quantistici al fine di verificarne proprietà temporali e spaziali.
Definizione di bisimulazioni, anche approssimate, per sistemi quantitativi e relativi algoritmi di decisione
Studio di un sistema a tableau a un passo, con struttura ad albero, per LTL e sue estensioni (aggiunta di operatori al passato, varianti prompt, LTL metrico, LTL interpretato su parole finite, LTL con forgettable past, estensioni di LTL con freeze quantifier).
Implementazioni efficienti di tale sistema e delle sue estensioni (parallelismo, integrazione con SAT solver, ..)
Model checking di sistemi a stati finiti (strutture di Kripke finite) e sistemi a stati infiniti (visibly pushdown system) con logiche ad intervalli con semantiche diverse (assunzione di omogeneità, uso delle espressioni regolari, grafo con transizioni etichettate con le relazioni di Allen).
Sviluppo di strumenti per la verifica di proprietà espresse in LTL per il linguaggio tccp, della famiglia dei linguaggi logici concorrenti con vincoli temporizzati, tipicamente usato per la modellazione di sistemi reattivi.
Studio di varianti ottimizzate di sistemi a tableau per vincoli su disuguaglianze lineari in domini numerici e di Herbrand usati nel meccanismo di verifica. Un prototipo di tali sistemi è disponibile all'URL http://safe-tools.dsic.upv.es/tadi/
Sviluppo di strumenti per la verifica di proprietà espresse in termini di approssimazioni delle risposte calcolate (mediante domini quali depth(k), POS, kPOS, ...) per i frammenti al prim'ordine dei linguaggi Haskell e Curry.
Studio di nuovi domini creati appositamente per modellare proprietà di interesse non esprimibili con i domini tradizionali. Studio di estensioni all'ordine superiore della tecnica del prim'ordine.
Sintesi. Studio del problema della sintesi per logiche ad intervalli espressive, estese o meno con una relazione di equivalenza. Applicazione dei risultati ottenuti a domini applicativi diversi (ad esempio, sintesi di controllori di piani e sintesi di gestori di workflow).

Settori ERC

PE6_4 Theoretical computer science, formal methods, automata
PE6_6 Algorithms and complexity, distributed, parallel and network algorithms, algorithmic game theory
PE6_3 Software engineering, programming languages and systems