RICERCA ITALIANA     

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

Università degli Studi di Padova

Abstract

La programmazione con vincoli e' un campo di ricerca multi-disciplinare in cui le competenze spaziano dalla Intelligenza Artificiale, alla Ricerca Operativa, ai Linguaggi di Programmazione, alle Basi di Dati, e le cui applicazioni sono presenti in molti discipline.

La programmazione con vincoli e' un paradigma di programmazione fondamentalmente diverso da molti altri, dato che richiede solo la modellazione di un problema in modo dichiarativo (specificando i suoi "vincoli") e poi la sua soluzione tramite una procedura generale che esplora lo spazio delle soluzioni e ne taglia parti inutili per mezzo di un uso attivo dei vincoli. Tipiche applicazioni della programmazione dei vincoli che hanno avuto molto successo sono i problemi di scheduling e di allocazione di risorse, i problemi di vehicle routing, gli orari, l'assegnamento delle frequenze. Nuovi campi applicativi che sono stati considerati negli ultimi anni sono
la bioinformatica, la configurazione online, la ricerca su web, e l'analisi di programmi e sistemi informatici.

La ricerca nel campo della programmazione con vincoli e' iniziata negli anni '70 nell'ambito dell'Intelligenza Artificiale e dal 1995 ha visto un aumento significativo dell'interesse sia teorico che pratico, con una conferenza internazionale annuale dedicata alla programmazione con vincoli, un'associazione internazionale, molti workshop e volumi,
una rivista internazionale, e cinque libri. L'Europa guida la ricerca in questo campo, ma molti altri gruppi sono sparsi per il mondo. In Italia, la ricerca nell'ambito della programmazione con vincoli e' svolta soprattutto dai gruppi coinvolti in questo progetto, che ha come uno degli scopi principali quello di far comunicare tali gruppi e incoraggiare la loro collaborazione, in modo da poter sfruttare le competenze comuni per una facile comunicazione, ma anche le competenze complementari per una fruttuosa collaborazione che porti a nuovi risultati sia teorici che pratici.

Piu' precisamente, l'obbiettivo di questo progetto e' quello di studiare estensioni dei formalismi e delle tecniche esistenti per la programmazione con vincoli, con particolare riferimento ad applicazioni innovative sia a sistemi informatici (es. sicurezza, analisi di programmi) che a problemi reali (es. scheduling,bioinformatica). Utilizzeremo quindi i vincoli come formalismo unificante, e le applicazioni come spunto per le estensioni
dei linguaggi e delle tecniche di risoluzione dei vincoli.

In particolare, studieremo come
-- estendere i formalismi per poter modellare preferenze positive e negative, condizionate e non, qualitative e quantitative
-- modellare e risolvere situazioni con piu' agenti, e studiarne le proprieta' fondamentali
-- sviluppare tecniche per situazioni con piu' criteri di ottimizzazione
-- gestire vincoli su intervalli e su insiemi.

I campi applicativi che considereremo sono:
-- soluzione di problemi di scheduling
-- verifica di proprieta' di sistemi concorrenti a stati infiniti
-- analisi di protocolli di sicurezza multilivello
-- bioinformatica.

Ogni unita' ha competenze comuni che finora sono state usate in modo indipendente ma complementare. Il progetto servira' a sfruttare
le competenze comuni e anche quelle complementari per ottenere risultati innovativi sia nell'ambito fondazionale e teorico, sia in quello applicativo. <<<

Coordinatore Scientifico del Programma di Ricerca

Francesca ROSSI Università degli Studi di PADOVA

Obiettivo del Programma di Ricerca

L'obbiettivo di questo progetto e' studiare estensioni dei formalismi e delle tecniche esistenti per la programmazione con vincoli, con particolare riferimento ad applicazioni innovative sia a sistemi informatici (es. sicurezza, analisi di programmi) che a problemi reali (es. scheduling, bioinformatica). Utilizzeremo quindi i vincoli come formalismo unificante, e le applicazioni come spunto per le estensioni dei linguaggi e delle tecniche di risoluzione dei vincoli.

Unita' di ricerca

Per ottenere questo obbiettivo, abbiamo coinvolto alcuni tra i principali gruppi di lavoro in questo ambito di ricerca in Italia, in modo da poter sfruttare le competenze comuni per una facile comunicazione, ma anche le competenze complementari per una fruttuosa collaborazione che porti a nuovi risultati sia teorici che pratici. Tali gruppi sono presenti anche in un ambito di ricerca internazionale, e producono regolarmente risultati sia teorici che applicativi che vengono ben accolti dalla comunita' internazionale e hanno dato luogo a nuove linee di ricerca all'interno della programmazione con vincoli. In particolare:
-- l'unita' 1 (Padova), che coordina questo progetto, ha forti competenze nell'ambito dei vincoli soft e delle preferenze, e anche nell'applicazione di tecniche di vincoli a problemi di scheduling;
-- l'unita' 2 (Udine) ha esperienza nella definizione e sviluppo di nuovi linguaggi di programmazione logica con vincoli su insiemi,
e anche nell'applicazione di tecniche di vincoli al problemi della bioinformatica e all'analisi di sistemi ibridi;
-- l'unita' 3 (Genova) contribuisce a questo progetto con le sue competeneze nell'ambito dell'analisi di sistemi informatici tramite tecniche basate sui vincoli;
-- l'unita' 4 (Pescara) ha competenze sia nello studio dei linguaggi logici e concorrenti con vincoli, che nell'applicazione di vincoli a problemi legati alla sicurezza.

Valore aggiunto del consorzio

Tutte le unita' hanno una profonda conoscenza delle tecniche di vincoli, e hanno rivolto la loro attenzione a diverse applicazioni utilizzando idee e tecniche correlate tra loro. Il valore aggiunto del consorzio e' rappresentato quindi dalla possibilita', attraverso una piu' stretta collaborazione e ad incontri organizzati durante lo svolgimento del progetto, di unire competenze anche complementari con lo scopo di consolidare e migliorare i risultati delle singole unita' e aprire nuove prospettive per le tecniche sviluppate nei rispettivi campi applicativi.

Linee di lavoro

Abbiamo percio' individuato delle linee di lavoro che permettano di fare cio', e che siano anche collegate tra loro in modo da favorire la tracimazione di risultati da una linea ad un'altra. In particolare, studieremo:

-- L'estensione di formalismi per poter modellare preferenze positive e negative, condizionate e non, qualitative e quantitative. In questo momento esistono molti formalismi per descrivere questi vari tipi di preferenze, ma nessuno che permetta di gestirne vari tipi allo stesso tempo.
Unita' coinvolte: Padova, Pescara.

-- La modellazione e soluzione di situazioni con piu' agenti, e lo studio delle loro proprieta' fondamentali. Questa sara' un'attivita' multi-disciplinare che usera' sia tecniche di intelligenza artificiale che di teoria delle decisioni.
Unita' coinvolte: Padova.

-- Lo sviluppo di tecniche per gestire situazioni con piu' criteri di ottimizzazione. Qui si useranno anche tecniche di ricerca operativa che sono molto utili in problemi di ottimizzazione.
Unita' coinvolte: Padova, Udine.

-- La gestione di vincoli su intervalli e su (multi)insiemi. Questa linea di lavoro estendera' l'applicabilita' della programmazione con vincoli in quegli ambiti dove e' naturale specificare vincoli su intervalli o su insiemi.
Unita' coinvolte: Udine, Genova.

I campi applicativi che considereremo sono:

-- Problemi di scheduling.
Si vuole poter gestire anche problemi con preferenze sulle attivita', e dove la soluzione ottenuta sia robusta alle modifiche del contesto.
Unita' coinvolte: Padova.

-- Verifica di proprieta' di sistemi concorrenti a stati infiniti.
Si vuole estendere lo stato dell'arte in questo campo tramite tecniche di vincoli e nozioni di composizionalita'.
Unita' coinvolte: Genova, Udine, Pescara.

-- Analisi di protocolli di sicurezza multilivello.
Si vuole usare i vincoli soft per poter modellare piu' fedelmente, e quindi risolvere in modo piu' soddisfacente, problemi tipici della sicurezza dei sistemi informatici.
Unita' coinvolte: Pescara, Genova.

-- Bioinformatica.
Si vuole sviluppare risolutori di vincoli ad hoc per alcuni problemi di bioinformatica, quali la predizione della struttura tridimensionale di una proteina.
Unita' coinvolte: Udine. <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

La Programmazione con Vincoli [MS98,D03,A03] e' una metodologia di programmazione che permette di formalizzare il problema da risolvere in modo puramente dichiarativo con l'ausilio di formule logiche dette appunto vincoli. La fase di computazione e' tipicamente basata sulla ricerca di una o più soluzioni che soddisfino l'insieme di vincoli imposti. La Programmazione con Vincoli permette di tenere ben distinte la fase di formalizzazione da quella di ricerca delle soluzioni. Tuttavia anche questa seconda fase viene guidata dai vincoli che devono essere rispettati, al fine di ridurre sensibilmente lo spazio di ricerca.

Un risolutore di vincoli e' una procedura effettiva in grado di determinare la soddisfacibilità di vincoli e di trovare soluzioni che li soddisfino tutti, se esistono. Diversi risolutori sono stati proposti dagli anni '80 in poi, per vari domini di vincoli e con proprietà e tecniche implementative diverse. Molti di questi stati proposti nell'ambito della Programmazione Logica con Vincoli (CLP) [JM94], dove attualmente i sistemi più utilizzati sono SICStus Prolog [SICS] ed ECLiPSe [ECLI] che mettono a disposizione svariati domini di computazione e corrispondenti risolutori e sono stati impiegati con successo nella risoluzione di problemi di ottimizzazione o di ricerca di soluzioni ammissibili per problemi in domini complessi e con funzioni obiettivo arbitrarie.

L'utilizzo di vincoli su domini finiti permette di formulare problemi di ottimizzazione combinatoria, quali problemi di scheduling, timetabling, etc. I risolutori di vincoli per tali domini sono basati sul concetto di propagazione di vincoli, utilizzando tipicamente la tecnica di arc consistency [M77] o sue semplificazioni, e sulla ricerca nello spazio delle soluzioni, controllata dalla propagazione dei vincoli che permette di rilevare assegnamenti parziali delle variabili che non possono condurre a soluzioni accettabili. Per problemi di ottimizzazione, la ben nota tecnica di branch-and-bound collabora con la propagazione di vincoli per diminuire il numero di soluzioni da investigare.

In molti problemi reali, non tutte le soluzioni sono ugualmente desiderate. Inoltre, in alcune situazioni i vincoli sono naturalmente associati a delle preferenze che rappresentano la gravità della loro violazione. Per poter modellare fedelmente queste situazioni, il formalismo classico dei vincoli e' stato generalizzato per permettere la descrizione di preferenze. Le preferenze non sono altro che dei vincoli nei quali, per ogni combinazione di valori alle variabili del vincolo, viene associato un elemento (la preferenza per quella combinazione) da un insieme ordinato (totalmente o parzialmente). Negli ultimi 10 anni sono nati vari formalismi per modellare e gestire problemi con preferenze, tra cui i piu' generali sono il formalismo basato sui semianelli [BMR97], quello dei valued CSP [SFV95], e le cosidette CP-nets [BBHP99]. Risolvere un problema con preferenze e' in genere piu' complesso che risolvere un problema di vincoli, in quanto ora le soluzioni volute sono solo quelle ottime rispetto alle preferenze. Tecniche di branch and bound, di propagazione di vincoli estesa alle preferenze, e di astrazione, sono utili per sviluppare un risolutore per problemi con preferenze.

Oltre alle preferenze, molti problemi reali presentano parti incerte, in cui l'utente non puo' decidere niente ma solo aspettare che le cose avvengano. Per questo e' importante poter gestire l'incertezza in problemi con vincoli e/o preferenze. Lo scopo e' allora trovare una o piu' soluzioni che siano buone secondo le preferenze ma anche sufficientemente compatibili con l'incertezza del problema. Vari formalismi per modellare l'incertezza sono stati proposti, a seconda del tipo di incertezza presa in considerazione. Ad esempio, si puo' pensare di associare ad ogni evento incerto una probabilita', o, in mancanza di una stima, un grado di possibilita' [Z78,DFP96].

L'ottimizzazione multi-obiettivo è considerata fondamentale in moltissime applicazioni reali. Tipicamente, nei problemi di ottimizzazione combinatoria presenti nel mondo industriale, è necessario ottimizzare più di un aspetto, in quanto gli obiettivi sono molteplici e non è sempre possibile raggrupparli in una sola funzione obiettivo. Spesso, poi, gli obiettivi sono discordanti, per cui una soluzione ottima per una certa funzione obiettivo può non esserlo per le altre. Il campo è vastissimo ed è stato affrontato in diverse comunità scientifiche: in Intelligenza Artificiale, ed, in particolare, in programmazione a vincoli [G02], e anche in ricerca operativa [EG00].

L'ottimizzazione multi-obbiettivo e' fortemente correlata con l'aggregazione di preferenze in sistemi multi-agente, dove una funzione di aggregazione deve decidere le soluzioni migliori per tutti [RVW04]. In tali scenari, soprattutto in ambito sociale, molti risultati di impossibilita' sono stati provati, riguardanti proprieta' come la fairness e la non-manipolabilita' [A51,G73].

Molti programmi applicativi della vita reale coinvolgono aspetti critici rispetto al tempo. Caratteristiche di tali applicazioni, usualmente dette sistemi integrati real-time, sono la specifica di vincoli temporali, come per esempio, la necessità di esprimere limiti superiori sul tempo di realizzazione di un evento (timeouts). Al fine di modellare tali situazioni un linguaggio deve permettere di specificare che in caso di timeout dovrà intraprendere un'azione alternativa. Sono stati sviluppati diversi formalismi per specificare, verificare e programmare sistemi reattivi, incluse le algebre di processo temporizzate, le logiche temporali e i linguaggi concorrenti con vincoli come il timed CCP [SJG96,DGM00].

Gli intervalli occupano un ruolo centrale nell'ambito della rappresentazione e del ragionamento temporali. Proprietà temporali significative di sistemi sviluppati in aree assai diverse, quali, ad esempio, la pianificazione, l'elaborazione del linguaggio naturale, la specifica e la verifica di sistemi hardware e software e la bioinformatica, possono essere descritte in modo naturale utilizzando formalismi basati sugli intervalli. Le logiche temporali basate su intervalli costituiscono uno dei più interessanti e sistematici approcci al trattamento degli intervalli temporali [GMS04].
E' stato recentemente proposto un metodo a tableau per la logica CDT interpretata sugli ordini parziali [GMSS05] che combina le caratteristiche dei metodi a tableau classici per la logica al prim'ordine con quelle dei metodi a tableau espliciti per le logiche modali, che prevedono un'apposita componente per la gestione dei vincoli sulle etichette.

Sono state studiate le possibilità concesse dall'utilizzo di vincoli di tipo insiemistico che permettono un elevato livello di astrazione in cui sviluppare prototipi funzionanti per un dato problema. E' stato descritto e implementato il linguaggio logico con vincoli CLP(SET) [DPPR00], oltre a diversi risultati nell'area dei risolutori di vincoli per insiemi/iperinsiemi, quali ad esempio [DPR98,DPR01]. In [DDPR03] CLP(SET) viene combinato con CLP(FD) per ottenere un linguaggio con vincoli su più domini che permetta di trarre vantaggio dalla dichiaratività dei vincoli insiemistici e dall'efficienza dei risolutori di vincoli su domini finiti. Recentemente è stato mostrato come il linguaggio CLP(SET) sia adatto a modellare e risolvere problemi di security [WWJ2004]. Membri dell'unità di Udine hanno recentemente sviluppato linguaggi tradizionali provvisti di vincoli insiemistici quali il Singleton [R02].

La programmazione con vincoli ha molte applicazioni. In questo progetto intendiamo studiare alcune di tali applicazioni, e migliorare la loro gestione attraverso nuove tecniche che svilupperemo in questo progetto.

1. Problemi di scheduling

Problemi di scheduling emergono in diverse situazioni reali [OPCC03,RDF05]. Infatti, tale problema puo' essere definito come l'assegnamento di tempi di inizio e di fine per un insieme di attivita' soggette a certi vincoli. I vincoli tipicamente sono di tipo temporale o di disponibilita' di risorse. La coordinazione della produzione in una azienda, la gestione di missioni spaziali, la schedulazione di trasporti sono esempi rappresentativi di problemi di scheduling. Oltre ai vincoli, di solito ci sono anche obiettivi e preferenze da ottimizzare. Quindi un problema di scheduling richiede di capire quando eseguire certe attivita' in modo che la soluzione finale garantisca buone performance.

2. Analisi statica e interpretazione astratta

Con il termine analisi statica si intende l'insieme delle tecniche per cui, dato un programma, si ricavano delle proprietà sulla sua futura esecuzione già a tempo di compilazione. L'Interpretazione Astratta e' un framework semantico per l'analisi statica di sistemi, introdotto da Patrick e Radhia Cousot in [CC79]. L'idea dell'interpretazione astratta e' quella di calcolare la semantica formale di un qualunque sistema, hardware o software, in un dominio astratto diverso da quello standard. Ogni oggetto del dominio astratto rappresenta un insieme di elementi del dominio concreto.

Ovviamente il risultato sarà solo una approssimazione della semantica effettiva, ma se il dominio è stato scelto con cura, questo può essere lo stesso sufficiente a ricavare informazioni rilevanti. Gran parte di questi risultati si è rivelato particolarmente utile nel campo dell'analisi statica di programmi logici, dove il dominio standard è
quello degli insiemi di sostituzione, che ha la struttura di un Sistema di Vincoli.

3. Model Checking simbolico

La tecnica di verifica detta Model Checking e' stata introdotta [CE81] come alternativa alle tecniche di simulazione fino ad allora utilizzate per convalidare hardware design. In questo ambito la specifica delle proprieta' di un sistema viene data attraverso il linguaggio della logica temporale [P81], mentre il modello della logica sottostante al funzionamento dei circuiti hardware e dei relativi protocolli di comunicazione viene descritto attraverso un sistemi di transizione. La procedura di model checking termina con successo se il sistema verifica la specifica, altrimenti restituisce una possibile esecuzione che viola uno dei suoi requisiti. Essendo basata sull'esplorazione dello spazio degli stati di un sistema, il maggior problema di questa tecnica e' la scalabilita' rispetto alla descrizione del sistema da verificare. Recentemente, l'applicazione di strutture dati dedicate per la rappresentazione di sistemi di transizione e insiemi di stati (BDD) ha permesso di estendere l'applicazione di tecniche di questo tipo a sistemi di grandi dimensioni. Questa idea ha dato origine alla tecnica cosiddetta di symbolic model checking [BCB+90].

Mentre i sistemi originariamente considerati dal model checking erano sistemi hardware e quindi intrinsecamente finiti, gli sforzi maggiori degli ultimi anni sono stati indirizzati verso lo sviluppo di modelli e algoritmi di verifica per sistemi con spazio degli stati potenzialmente infinito, come in [AH92,MCJ97,ACJT96,ACH+95,AJ03]. Le idee principali sottostanti le tecniche di model checking possono essere estese direttamente al caso di sistemi infiniti. In molte di queste estensioni il concetto di base e' la rappresentazione di insiemi di stati tramite linguaggi con vincoli, che ha dato vita al paradigma chiamato constraint-based model checking. I vincoli vengono utilizzati come linguaggio asserzionale [KMMPS01] per rappresentare collezioni infinite di configurazioni di un sistema concorrente. Le operazioni sui vincoli sono utilizzate quindi all'interno degli algoritmi basati su computazioni di punto fisso sui quali si basa la tecnica di model checking.

Un altro approccio alla verifica di sistemi a stati infiniti, che e' automatico sebbene incompleto, utilizza la programmazione logica con vincoli per specificare i sistemi reattivi e le loro proprieta', e la specializzazione dei programmi come meccanismo di inferenza per la verifica delle proprieta' d'interesse. Con queste tecniche sono state provate proprieta' di safety e di liveness per vari protocolli a stati infiniti [FPP02,FPP04].

Negli ultimi anni sono state trovate numerose applicazioni per le tecniche di verifica basate su vincoli. In molte di queste applicazioni la tecnologia basata su vincoli viene combinata con astrazioni definite sia al livello della descrizione del sistema [D00,DB01] che al livello della rappresentazione simbolica delle configurazioni [BD02a].

Una delle direzioni piu' interessanti nel campo dell'applicazione dei vincoli all'analisi di sistemi infiniti riguarda l'analisi di sistemi con tipi di dato eterogenei e di sistemi aperti quali i web services. In questo ambito sembra interessante studiare la combinazione di vincoli con tecniche di composizionalita' e con la teoria dei giochi.

4. Verifica di Sistemi Ibridi

Gli Automi Ibridi sono stati introdotti in [ACHH92] come linguaggio di modellazione e specifica per sistemi ibridi, ovvero sistemi in cui un programma discreto interagisce con un ambiente a variazioni nel continuo, e sono stati ampiamente utilizzati per la verifica automatica di sistemi sia di tipo ingegneristico che di tipo biologico.

Uno stato dell'automa ibrido e' individuato da uno stato della componente discreta e da un assegnamento di valori reali per le componenti continue. Si vuole caratterizzare l'insieme degli stati raggiungibili attraverso transizioni discrete e continue dagli stati iniziali.

Tra gli approcci proposti per lo studio di automi ibridi emergono approcci simbolici basati sulla traduzione dell'automa in vincoli sui reali e sullo sviluppo di risolutori per tali vincoli. Gli approcci simbolici si fondano sulla decidibilita' delle formule al primo ordine sulla teoria dei reali, provata in [T51]. Recentemente [RS05] suggerisce un nuovo metodo di raffinamento astratto basato su propagazione di vincoli per la verifica di sistemi ibridi con equazioni differenziali autonome.

5. Sicurezza

La sicurezza di una rete e' basata non solo sulla sicurezza delle sue componenti e delle interconnessione dirette tra loro, ma anche sulla potenziale possibilita' che i sistemi possono avere di interoperare indirettamente attraverso le connessioni di rete. Tale possibilita' puo' infatti potenzialmente creare dei "cascading path" che violano la sicurezza dei sistemi attraverso le connessioni di rete. In [BFO04] e'
mostrato come la programmazione con vincoli fornisce un approccio naturale per esprimere i vincoli necessari per assicurare la sicurezza multilivello attraverso la rete. In particolare i vincoli soft possono essere usati per evidenziare ed eliminare i cascading path nella rete che violano la sicurezza ed ottenere una soluzione minimale (anche se non ottima) in tempo polinomiale. I vincoli soft migliorano anche l'analisi delle politiche di integrita' [BF03a,BF03b].

6. Bioinformatica

Recentemente diversi problemi di Bioinformatica sono stati mostrati essere codificabili come problemi di vincoli su domini finiti [CB01]. In particolare, il problema di determinare la conformazione tridimensionale di una proteina una volta nota la sequenza di amino acidi che la compongono(Protein Folding) e' stato codificato come problema vincolato su un dominio discreto (il cubo a facce centrate) usando funzioni di energia approssimate (il modello HP) [BW01].

Il problema del protein folding e' affrontato con vari metodi, ma in particolare mediante simulazione. Seppure precise dal punto di vista termodinamico, tali simulazioni sono estremamente lente. Recentemente e' stato mostrato come sia naturale scrivere delle simulazioni in Concurrent Constraint Programming in cui gli elementi di base sono dei processi concorrenti associati ad ogni aminoico costituente la proteina [DDF04a]. <<<