RICERCA ITALIANA     

Programma di ricerca

Vincoli e preferenze come formalismo unificante per l'analisi di sistemi informatici e la soluzione di problemi reali

Università di riferimento

Università degli Studi di UDINE - MATEMATICA E INFORMATICA - UDINE(UD)

Responsabile dell'Unità di ricerca

Agostino DOVIER

Descrizione

L'unità di ricerca di Udine articolerà il proprio contributo alla ricerca nei seguenti quattro filoni:

1. VINCOLI E INSIEMI
2. VINCOLI E AUTOMI
3. VINCOLI E INTERVALLI
4. VINCOLI E BIOINFORMATICA

Nel filone dei VINCOLI E INSIEMI si intende procedere ad investigare le problematiche connesse alla progettazione ed alla integrazione di linguaggi di programmazione con vincoli di tipo insiemistico/iperinsiemistico/multiinsiemistico con particolare attenzione agli aspetti computazionali che garantiscano la loro effettiva utilizzabilità. In particolare si desidera analizzare le problematiche relative alla integrazione o cooperazione dei risolutori di vincoli insiemistici di CLP(SET) e a quelli su domini finiti di CLP(FD). Ciò permette di ottenere un ambiente di programmazione con vincoli che permette la dichiaratività della programmazione insiemistica, adatta alla rapida prototipazione del software e l'efficienza data dai risolutori su domini finiti. Si desidera inoltre, usando tecniche di interpretazione astratta, sviluppare dei compilatori di parti di codice CLP(SET) in CLP(FD).

Si desidera inoltre completare e mettere a punto la libreria JSetL, una libreria Java che offre caratteristiche proprie dei linguaggi logici a vincoli, in particolare con vincoli insiemistici, in un ambito di programmazione "object-oriented". In questo contesto verrà anche affrontato il problema della cooperazione di più risolutori di vincoli, utilizzando ed adattando tecniche di "cooperative constraint solving" note in letteratura, allo specifico ambiente offerto da JSetL. Questo porterà tra l'altro ad una riprogettazione dell'architettura complessiva di JSetL, che, sfruttando i meccanismi di multitasking e comunicazione tra processi offerti da Java, permetta una strutturazione del sistema che faciliti l'integrazione tra diversi risolutori di vincoli.

Una metodologia di programmazione dichiarativa che sta riscuotendo un crescente interesse è l'Answer Set Programming (in breve, ASP). I programmi ASP sono programmi logici privi di simboli funzionali ma con arbitraria presenza di letterali negati. Per tali programmi l'esistenza di un modello non garantita; modelli interessanti sono i modelli stabili [GL88] per il calcolo dei quali sono stati sviluppati opportuni risolutori (p. es., SMODELS, DLV, ASSAT). E' dimostrato che la classe dei problemi codificabili mediante ASP equivale esattamente alla classe NP [MT91]. Pertanto nei risolutori di ASP vi sono tecniche di risoluzione simili a quelle utilizzate, ad esempio, nei risolutori di vincoli CLP(FD) che tipicamente affrontano problemi simili. Per la codifica di problemi con vincoli, la metodologia ASP va dunque tenuta in cosiderazione. Nell'ambito del progetto si desidera integrare le idee utilizzate nei risolutori per answer set programming e nei risolutori per vincoli su domini finiti in CLP(FD) in un unico risolutore adatto ad affrontare, in generale, problemi NP-completi.

Nel filone VINCOLI E AUTOMI, studieremo il problema della decidibilità per opportune varianti ed estensioni delle classi di automi considerate nella base di partenza; in particolare, le loro proprietà di chiusura. Inoltre, affronteremo il problema di determinare le controparti logiche di tali classi di automi. Ciò consentirà di usare le prime come un'interfaccia di alto livello per la specifica dei sistemi e/o delle loro proprietà e i secondi come un formalismo di basso di livello per eseguire la verifica. Dedicheremo particolare attenzione all'utilizzo di tecniche di programmazione con vincoli per gestire in modo efficiente i vincoli (temporali). Oltre che in ambito biologico, intendiamo sperimentare tali strumenti in altri contesti applicativi, quali quello delle basi di dati temporali e spaziali, quello dei sistemi di workflow e quello più tradizionale dei sistemi reattivi e in tempo reale richiamati in precedenza. Intendiamo inoltre sviluppare un confronto sistematico tra le soluzioni da noi proposte, che sfruttano le potenzialità offerte dalla nozione di vincolo, e gli approcci ai sistemi a stati infiniti presenti in letteratura (approccio trasformazionale, sviluppato da Caucal e altri, sistemi di riscrittura, sistemi equazionali, uso di transducer).

Per quanto riguarda lo studio degli automi ibridi, un problema fondamentale è quello della raggiungibilità. Uno stato dell'automa ibrido è individuato da uno stato della componente discreta e da un assegnamento di valori reali alle componenti continue. Si vuole caratterizzare l'insieme degli stati raggiungibili attraverso transizioni discrete e continue dagli stati iniziali [Alu92]. Tra gli approcci proposti per lo studio di automi ibridi emergono approcci simbolici basati sulla traduzione dell'automa in vincoli (formule) sui reali e sullo sviluppo di risolutori per tali vincoli. Gli approcci simbolici si fondano sulla decidibilità delle formule al primo ordine nella teoria dei reali provata da Tarski in [Tar51]. Citiamo come esempi [Ana99] e [Fra99] che hanno indipendentemente suggerito l'utilizzo dell'eliminazione dei quantificatori per la verifica di sistemi ibridi polinomiali. [Fra04] ha sviluppato "sistemi di prova" per il bounded model checking di questi sistemi. [Laf01] propone un metodo basato sull'eliminazione dei quantificatori per il calcolo della raggiungibilità simbolica nel caso di campi vettoriali lineari. [RS05] ha suggerito un nuovo metodo di raffinamento astratto basato su propagazione di vincoli per la verifica di sistemi ibridi con equazioni differenziali autonome.
Tali tecniche di verifica simbolica sono attualmente applicabili a classi molto ristrette di automi ibridi. Spesso si considerano sistemi di equazioni differenziali lineari [Laf01], o comunque sistemi autonomi per i quali è possibile dimostrare esistenza ed unicità della soluzione [Laf00]. In molti casi questi automi ibridi sono traducibili in un unico sistema di equazioni differenziali [PM05] e tecniche sviluppate in analisi possono essere utilizzate per il loro studio. Queste assunzioni non bastano per assicurare la convegenza del processo di traduzione in vincoli [Fran01].
Si intendono pertanto scoprire delle ipotesi sugli automi ibridi che garantiscano la convergenza della traduzione in vincoli sui reali, ovvero ipotesi che garantiscano di ottenere un'unica formula e non una sequenza infinita di formule. Le ipotesi che intendiamo studiare saranno ottenute come combinazione di restrizioni sulla componente continua e sulla componente discreta del sistema. Tale combinazione dovrebbe consentire di studiare anche sistemi di inclusioni differenziali non autonomi. Si intende inoltre analizzare in quali casi i vincoli ottenuti dalla traduzione possono essere verificati in modo efficiente o possono essere approssimati con limitazioni sull'errore. Recentemente sono stati proposti numerosi metodi [Gri88, Ren92, Bas97] che aumentano l'applicabilità del risultato di decidibilità di Tarski [Tar51] abbassandone la complessità per particolari classi di formule. Tuttavia numerose tecniche di geometria algebrica quali le basi di Groebner a gli insiemi caratteristici non sono ancora state pienamente sfruttate.
Infine, si desidera implementare un tool in grado di effettuare la traduzione e la verifica eventualmente interfacciandosi con tool già esistenti per la verifica di vincoli sui reali, come ad esempio QepCad.

Nell'area del filone VINCOLI E INTERVALLI, si intende trasformare il metodo a tableau proposto in [Gor03b,Gor05] in una procedura di decisione per classi particolari di logiche temporali, quali la famiglia delle Split Logic (SL) [MSV02] e la famiglia delle Propositional Neighborhood Logic (PNL) [Gor03a,Gor03c].

In particolare, verranno esplorate opportune restrizioni di tipo sintattico o semantico, che garantiscano la terminazione del processo di costruzione e verifica del tableau. Per quanto riguarda le restizioni sintattiche, si imporranno delle condizioni sul numero e la tipologia degli operatori temporali utilizzati; per quanto riguarda le restrizioni semantiche, si imporranno opportune condizioni sulla struttura temporale (strutture finite, strutture split, strutture discrete, numeri naturali) e/o sull'interpretazione (ad esempio, il principio di localita'). Esempi di logiche decidibili ottenute imponendo tali restrizioni sono riportati in [Gor04].

Di recente, abbiamo ottenuto dei risultati preliminari promettenti per il frammento della logica PNL che contiene i soli operatori futuri, vale a dire gli operatori che consentono di predicare solo sugli intervalli alla destra dell'intervallo corrente, interpretato sul dominio dei naturali. L'approccio proposto combina restrizioni sintattiche (operatori temporali: frammento futuro) e restrizioni semantiche (struttura temporale: numeri naturali) e verrà utilizzato com punto di partenza per lo studio della decidibilita' di altre logiche ad intervalli, quali, ad esempio, la logica PNL completa, interpretata sui naturali o su altre classi di strutture temporali, e la logica dei sottointervalli, o logica D, il cui unico operatore temporale consente di esprimere la relazione di inclusione tra intervalli. Studieremo, inoltre, gli effetti dell'introduzione della restrizione alle sole intepretazioni/modelli finite su logiche che, senza tale restrizione, sono state dimostrate indecidibili, sulla base di risultati ottenuti di recente da Pratt [Pra05].

Infine, per supportare in maniera adeguata il lavoro di sviluppo, testing e validazione di tali procedure, verranno utilizzate tecniche e strumenti mutuati dalla programmazione (logica) con vincoli. Le procedure di decisione così ottenute verranno sperimentate in ambito biologico per la specifica e la verifica di rilevanti proprietà temporali, in linea con quanto fatto in [Vit05].

Nel filone VINCOLI E BIOINFORMATICA tre saranno le tematiche principali su cui si focalizzerà il lavoro dell'unità di Udine.

La prima di queste riguarda la predizione della struttura tridimensionale di una proteina data le sequenza di aminoacidi che la compongono. Si intende affrontare tale problema come problema di minimizzazione di una funzione di energia le cui variabili siano le posizioni spaziali dei centri degli aminoacidi che possono assumere valori su alcuni punti di un reticolo discreto, principalmente il Face Centered Cubic (FCC) lattice. La funzione di energia da minimizzare dipende dalle distanze tra i vari aminoacidi e dai tipi di aminoacidi in gioco. In particolare, ci si vuole concentrare sullo sviluppo di un risolutore di vincoli ad hoc per vincoli su reticoli adatti a discretizzare le proteine, al fine di ottimizzare il codice presentato in [BMC04]. Il codice, da svilupparsi in C++, andrà a rimpiazzare il risolutore di vincoli su domini finiti del SICStus Prolog attualmente utilizzato per tale problema. La disponibilità delle strutture dati a basso livello permetterà di programmare in modo efficiente nuove euristiche per il problema. Sarà inoltre possibile utilizzare la metodologia a vincoli per determinare il ripiegamento di grosse proteine costituite da sequenze di proteine note e più piccole. Si tratta, dunque, di vedere queste ultime come corpi rigidi di cui si vuole trovare la posizione spaziale che minimizza la funzione di energia globale. Tale approccio non risulta attualmente praticabile con i risolutori disponibili in SICStus Prolog a causa dell'elevato numero di variabili in gioco. I codici prodotti saranno poi portati su macchina parallela.

La seconda tematica di questo filone riguarda sempre il problema del protein folding, ma sarà affrontato in modo diverso. Anzichè utilizzare un reticolo discreto, si lasceranno le proteine libere di assumere ogni posizione nello spazio e la minimizzazione della funzione d'energia avviene per mezzo di una simulazione concorrente. In questo contesto si desidera investigare l'applicabilità del modello di ottimizzazione multiagente [MR04] al nostro problema e la sua possibile generalizzazione ad altre simulazioni biologiche. In questo contesto si desidera passare da una formalizzazione nel linguaggio di coordinamento Linda ad un modello basato su MPI che permetta una effettiva computazione concorrente su Cluster di PC.

La terza tematica del filone VINCOLI E BIOINFORMATICA è costituita dalla simulazione e verifica di sistemi biologici e sarà basata sull'utilizzo dei risultati del filone VINCOLI E AUTOMI sopra descritto.