Logics, Automata and Automated Verification

Cluster

Theoretical Computer Science

Description

The research themes the group is interested in range across several areas that can be grouped as follows:

Temporal Logics for Informatics. Using temporal logics based on points or intervals as languages for the specification, automatic verification and synthesis of complex models. Decidability and complexity of satisifiability problems, of model checking and synthesis. Formalisation and solution of informatic problems (for instance, the automated planning problem) by means of temporal logic systems.
Automi. Automata. Definition and analysis of suitable classes of automata with counters in order to express properties not captured by omega-regular languages. Modelling through hybrid automata of systems involving discrete and continuous components. Identification of decidable classes of hybrid automata. Analysis of temporal properties on hybrid automata. Analysis of parametric systems. Verification of temporal properties of quantum protocols and algorithms. Contraction algorithms through simulation/bisimulation. Numerical encoding of automata.
. Verification of Satisfiability. Decidability and computational complexity of the satisfiability problem for interval temporal logic with regard to different semantics (with or without point intervals, with or without the assumption of homogeneity). Development and implementation of tableau systems for interval temporal logic. Development and implementation of alternative tableau systems for linear temporal logic (LTL) and for its various extensions, and comparison with alternative decision-making procedures (based on automata, through solution, by means of algorithms for symbolic model checking).
Verification of Observational Equivalence. Bisimulations on Labeled Transition Systems (LTS), especially with reference to safety issues, and related decision-making algorithms. Bisimulation for LTS with quantitative aspects and discrete-time or continuous-time Markov chains. Lumping algorithms.
Model Checking. Model checking for finite-state systems and infinite-state systems by interval temporal logics with respect to different semantics. Comparison between model checking of point-based temporal logics (LTL, CTL and CTL*) and model checking of interval temporal logics.
Abstract Interpretation. Verification by means of abstract interpretation for reactive systems. Development of tools for verifying properties expressed in LTL and its extensions. Study of variants of tableau systems for constraint systems that underpin the verification engine of such tools. Verification through abstract interpretation for functional and logic-functional languages. Development of tools for the verification of properties of computed answers in approximate domains, both those typical in literature and specifically developed ones.
Synthesis. Study of the synthesis problem for interval logics, and for their extensions with an equivalence relationship, with respect to finite linear orders and the domain of naturals. Characterisation of the problem by means of logic games.

Research subjects

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).

ERC panels

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