MINISTERO DELL'UNIVERSITÀ E DELLA RICERCA SCIENTIFICA
PROGRAMMI DI RICERCA - ANNO 2006

Obiettivo della Ricerca

Il nostro scopo nel lungo termine è duplice. Anzitutto, miriamo a scoprire nuovi modelli e teorie dell’informatica ispirate dal mondo biologico e a produrre tecniche e strumenti per trattare problemi informatici molto più complessi di quelli trattabili con la tecnologia corrente. In secondo luogo, ci proponiamo di fornire ai biologi un ambiente per studiare a livello di sistema problemi non affrontabili senza l’uso dell’informatica. Questo ambiente offrirà ai biologi strumenti di modello, di analisi e di simulazione capaci di trattare comportamenti complessi e di rappresentare proprietà emergenti.

Noi auspichiamo perciò una convergenza tra le scienze dell’informazione e quelle della vita e ci collochiamo sul lato informatico della Biologia dei Sistemi. Questo paradigma emergente muove dal classico approccio riduzionistico verso una comprensione della vita a livello di sistema, dove appaiono comportamenti impredicibili e complessi. Essenziale per questo cambiamento è lo spostamento di attenzione che sta avvenendo da struttura a funzionalità. Poiché le scienze dell’informazione hanno come oggetto di studio le modalità di funzionamento dei sistemi, a differenza della matematica o della fisica che guardano solo al risultato, esse saranno di grande aiuto per sviluppare una teoria del funzionamento di sistemi biologici , visti come insiemi di processi di calcolo. Nella nostra terminologia, passare da struttura a funzione equivale ad equipaggiare la sintassi con una semantica comportamentale. Auspichiamo cosí uno spostamento di paradigma anche sul versante bioinformatico: ci proponiamo di costruire modelli, linguaggi e strumenti per descrivere, analizzare e realizzare in silico sistemi biologici, sviluppando un settore di ricerca che si aggiunge ad altri tipici della bioinformatica attuale, quali lo studio di tecniche per memorizzare, organizzare e ritrovare grandi quantità di dati biologici o ricercare e confrontare sequenze di DNA, per menzionare due argomenti noti.

Più in dettaglio, svilupperemo e useremo metodi formali per modellare e studiare il comportamento della materia vivente. Partiremo dal fatto che i sistemi biologici sono spesso descritti come entità che cambiano di stato a seguito di interazioni bio-chimiche, dando luogo a un comportamento osservabile. Proprio nello stesso modo, i sistemi di calcolo sono presentati come macchine astratte, il cui comportamento è specificato da transizioni tra gli stati interni della macchina astratta. Aderiamo cosí alla visione della materia vivente come unità di calcolo biologica. Seguiremo tre principali linee di ricerca, e ciascuna di esse affronterà aspetti complementari delle macchine astratte.

La prima linea consiste nello sviluppo di nuovi calcoli di processo, dotati di primitive bio-mimetiche, con particolare attenzione all’interazione tra processi e agli aspetti stocastici e probabilistici. Tali primitive rifletteranno il modo in cui gli organismi viventi interagiscono con altre entità o con l’ambiente. I nostri calcoli condivideranno con quelli esistenti la semantica formale, eseguibile, consentendo cosí di riutilizzare teorie, metodi e strumenti assodati. Di particolare rilievo sono gli interpreti che consentono di eseguire la specifica di un organismo biologico, in modo che ciascuna esecuzione può essere vista come un esperimento in silico. Naturalmente parametri stocastici sono di grande importanza per tali simulazioni, cosí come strumenti statistici per ulteriori analisi del comportamento simulato.

La seconda linea di ricerca considererà approcci misti alla biologia dei sistemi, tra cui una teoria composizionale degli automi ibridi, un approccio algebrico al model checking e lo sviluppo di un meta-strumento per tale analisi. Studieremo i rapporti tra calcoli di processo e automi ibridi, chiarendo le relazioni tra descrizioni di sistemi biologici interne, cioè basate su comunicazione, ed esterne, cioè basate su quantità osservabili descritte principalmente da equazioni differenziali. L’interesse per metodi composizionali su automi ibridi nasce dal fatto che i sistemi reali hanno molti componenti che interagiscono tra loro e che i loro modelli hanno un numero di stati esponenziale rispetto al numero dei componenti (state explosion problem). Le tecniche proposte per ovviare a questo problema son tutte top-down: si riduce lo spazio degli stati dell’intero sistema. Noi cercheremo invece un approccio bottom-up, in cui si verifichino i singoli componenti e si combinino i risultati per ottenere il risultato globale; studieremo inoltre le condizioni in cui esso sia applicabile. Useremo risultati di Tarski e l’eliminazione di quantificatori per studiare automi ibridi, lungo una linea molto seguita negli ultimi anni. Seguiremo un approccio algebrico nel dominio biologico al fine di determinare classi di automi ibridi decidibili, e tecniche di model checking approssimate basate su vincoli fisici dei sistemi e decomposizioni parziali di algebre cilindriche.

La terza linea di ricerca è ispirata dal funzionamento della cellula, in particolare dai processi che regolano la trasmissione di sostanze biochimiche attraverso le membrane. Useremo i Membrane Systems per modellare e simulare le attività dei vari canali proteici transmembranici delle cellule, con l’obiettivo di valutare quanto i P systems siano adeguati nel descrivere specifiche funzionalità cellulari. Il nostro scopo è quello di allargare l’applicabilità del Membrane Computing e di stimolare ulteriori collaborazioni tra microbiologi e gli esperti di P systems. Progetteremo simulatori per verificare la bontà dei nostri modelli. Poiché piccole variazioni nelle condizioni al contorno provocano cambiamenti nei parametri e nel comportamento di sistemi complessi, considereremo modelli con regole dinamiche dotate di informazioni probabilistiche che possano cambiare nel tempo. Questi modelli stocastici appaiono migliori di quelli basati su equazioni differenziali quando vi siano basse concentrazioni di reagenti in molti processi attivi contemporaneamente.

Le nostre idee e le nostre proposte saranno messe a punto, collaudate e convalidate su alcuni casi di studio provenienti dalla letteratura e selezionate con i biologi che fan parte di tutte le unità di ricerca, e anche con biologi e informatici attivi internazionalmente, con i cui risultati ci confronteremo. La fattibilità del nostro approccio sarà inoltre verificata progettando e realizzando alcuni strumenti software prototipali, compatibilmente con le scarse risorse assegnateci, i quali saranno basati sulle teorie che andremo sviluppando nella prima fase del lavoro.

Innovazione rispetto allo stato dell'arte nel campo

Se il progetto avrà successo, avremo una conferma del comune sentire che l’informatica sarà indispensabile per la biologia, e viceversa, cosí come è avvenuto per la matematica e la fisica. In ogni caso ci sarà un arricchimento reciproco tra informatica e biologia. I biologi potranno fare esperimenti in silico per meglio comprendere le funzioni delle cellule al livello di dettaglio voluto, e potranno auspicabilmente predirne il comportamento e scoprirne aspetti nuovi. Gli informatici guadagneranno una migliore conoscenza sui metodi formali per descrivere e analizzare sistemi di calcolo complessi, quali quelli che vediamo quotidianamente sul web, con una ricaduta quasi immediata sull’importante campo dei servizi e delle applicazioni in rete.

Piú in dettaglio, gli aspetti innovativi riguarderanno i punti seguenti.

Particolaremente rilevante è lo sviluppo di calcoli per la descrizione di cellule biologiche. Le loro primitive di comunicazione e di interazione ispirate dalla biologia potrebbero aiutare a definire sistemi piú efficienti ed affidabili di agenti di calcolo mobili e concorrenti. Uno dei principali aspetti innovativi sarà la definizione di un paradigma di interazione che tenga conto della specificità delle interazioni biologiche che dipendono, e.g., da fattori quali l’energia, l’affinità chimica, la distanza fisica tra particelle, la loro carica elettrostatica, ecc. Tale definizione corrisponde a una modalità di comunicazione intrinsecamente stocastica, piuttosto che deterministica e/o non-deterministica.
Gli aspetti stocastici, temporali, probabilistici e generalmente quantitativi dei calcoli studiati rappresenteranno un avanzamento rispetto quelli descritti in letteratura; inoltre, vi saranno nuove tecniche formali di verifica delle proprietà del sistema biologico modellato, sviluppate per questi modelli e per le loro estensioni quantitative.
Nuovi risultati riguarderanno il confronto del potere espressivo dei calcoli per processi biologici proposti da noi e da altri gruppi attivi nel campo.
La definizione di equivalenze comportamentali ispirate alla biologia e a comportamenti di tipo stocastico, permettendo la minimizzazione del numero di stati corrispondenti al comportamento dei processi del linguaggio, sarà uno strumento particolarmente utile all’automazione dell’analisi del comportamento dei sistemi descritti.

Attualmente non sono disponibili in letteratura tecniche generali che permettano l’intertraducibilità tra modelli discreti e stocastici (algebre di processo stocastiche) e modelli continui e deterministici (sistemi di equazioni differenziali), in quanto le proposte esistenti riguardano essenzialmente il caso con rate stocastici costanti. Tali relazioni dicreto/stocastico sono essenziali in applicazioni, quali quelle alla biologia, dove c’è una ben stabilita tradizione di sviluppo di modelli continui.

L’uso della logica temporale per la specifica di criteri di confronto comportamentale tra le diverse tipologie di simulazioni è importante. Tali criteri costituiranno la parte essenziale della verifica delle metodologie e consentiranno l'utilizzo di tecniche automatiche quali il model-checking e gli algoritmi di raggiungibilità in questo contesto.

Un aspetto innovativo riguarda lo sviluppo di alcuni strumenti di supporto di nuova concezione, tra cui:
- animatori e interpreti dei calcoli, con i vari aspetti quantitativi, per la simulazione in silico di processi cellulari;
- strumenti per la raccolta di dati sperimentali in silico e per la loro analisi numerica;
- strumenti per l’analisi simbolica, quali controllori di equivalenze e model-checker;
- strumenti open source per l'analisi di raggiungibilità in sistemi ibridi che supportino il plug-in di metodi di analisi e un'arbitraria precisione nella analisi delle dinamiche.

Una potenziale ricaduta sul campo stesso della biologia riguarda il fatto che l’auspicata corrispondenza dei comportamenti in silico con omologhe osservazioni in vivo potrebbe rappresentare una conferma decisiva della validità dei modelli individuati, e aprire la strada all’utilizzo di una cellula virtuale a scopo predittivo. La simulazione dinamica in condizioni perturbate permetterà di esaminare in silico la possibilità di attivazione di vie metaboliche alternative a quelle bloccate,e l’insorgenza di percorsi metabolici non esplicitamente descritti dalla biochimica classica.
Inoltre, vediamo come innovative le proposte di sviluppare tecniche di machine learning e di algoritmi genetici per analizzare dati di genomica strutturale con paradigmi probabilistici, per inferenze di natura strutturale a partire dall'informazione incapsulata a livello di sequenze di DNA.
Infine, lo sviluppo di tecniche di analisi di dati di espressione genica da microarray che sfruttano la conoscenza biologica espressa in modelli computazionali permettera’ l’utilizzo diretto (p.e. in forma di ipotesi, indicazioni per il controllo di qualità o intervalli di espressione attesa) dei risultati di simulazioni temporali svolte su modelli computazionali di sottosistemi biologici noti. I risultati attesi sono: una tecnica di analisi efficace, verifica dell’efficacia delle tecniche di modellazione per il supporto all’analisi di dati di espressione genica, indicazioni di eventuali modifiche ai formalismi usati.

Criteri di verificabilità

1. quantità e qualità delle pubblicazioni, misurata anche dalla rilevanza scientifica e dalla diffusione della collocazione editoriale

2. visibilità dei membri, valutata anche sulla loro capacità di organizzare eventi scientifici, di essere invitati a partecipare a comitati scientifici, ecc.

3. collaborazioni e interazioni tra le U.O. e con gruppi di lavoro nazionali e internazionali nel settore e in aree affini

4. produzione di strumenti software

Elenco delle Unità di Ricerca

Sede dell'Unità:  Università degli Studi di UDINE

Compito dell'Unità

I compiti dell'unità di Udine riguarderanno i seguenti quattro punti:

Teoria composizionale degli automi ibridi.
Per affrontare problema della complessità nell'ambito della simulazione in biologia, useremo metodi continui e discreti per la simulazione. Mediante automi ibridi, individueremo le proprietà degli automi che necessarie a garantire forme di composizionalità nella verifica.

Approccio algebrico al model checking di sistemi biologici
Proporremo metodologie di model checking e verifica per sistemi biologici modellati mediante automi ibridi. Partiremo dalle metodologie basate sulla rappresentazione semi-algebrica e dal metodo di eliminazione dei quantificatori originariamente
introdotto da Tarski. Proseguiremo studi precedenti su esempi concreti di modelli
biologici rappresentabili mediante interazioni discrete e continue e verificabili tramite metodi di decomposizione quali quelle per decidere la teoria dei reali.

Ariande: a meta-tool for hybrid automaton model checking.
Svilupperemo e applicheremo l'ambiente per la verifica dei sistemi ibridi Ariadne. I tre obbiettivi principali di Ariadne sono: realizzare un ambiente di sviluppo in cui definire tecniche di rappresentazione dello spazio e algoritmi per l'analisi di raggiungibilità; definire un software che integri e implementi algoritmi e tecniche di rappresentazione esistenti consentendo all'utente di sceglierne i piú adatti; supportare la rappresentazione approssimata in precisione arbitraria dell'evoluzione di un automa ibrido. Ariadne, offrirà uno schema ad alto livello basato su moduli generali, in modo da consentire una più facile personalizzazione. Il pacchetto sarà rilasciato come open source in modo che differenti gruppi di ricerca possano contribuire al progetto con nuove strutture dati, algoritmi e euristiche. Ariadne, implementerà i principali metodi geometrici per rappresentare lo spazio, basati su simplex, parallelotopi, zonotopi e poliedri parametrizzandoli sui reali. Ariadne consentirà all'utente di definire funzioni multivariate dell'insieme degli oggetti rappresentabili a se stesso e fornirà metodi di valutazione per esse.

Approccio misto algebre dei processi - automi
Svilupperemo metodologie per modellare situazioni biologicamente significative, connettendo algebre di processo e automi ibridi. Studieremo corrispondenze tra i primi e i secondi, per chiarificare la espressività relativa tra una descrizione interna (basata sulla comunicazione) e una esterna (basata su quantità osservabili principalmente mediante sistemi di equazioni differenziali) dello stesso sistema biologico. Tale corrispondenza dovrà esser stabilita dimostrando risultati di transfer che permettano p.e. di passare da una rappresentazione mediante il pi-calcolo stocastico e una rappresentazione basata su sistemi di equazioni differenziali, p.e. gli S-sistemi di Voit o le Generalized Mass Action equations di Savageau.

Il punto chiave sarà di far corrispondere i due precendenti formalismi per consentire un uso ottimale delle loro possibilità espressive in senso quantitativo. Questo passo è un prerequisito necessario per un legame più fondamentale tra descrizione mediante algebre di processo e automi ibridi, in quanto caratterizzerebbe la dinamica della parte continua del comportamento del sistema oggetto di studio. Tale passo sarà poi seguito dalla determinazione della parte discreta dell'automa, che caratterizza il controllo discreto del sistema biologico sulla sua dinamica.

Sede dell'Unità:  Università degli Studi di PISA

Compito dell'Unità

L'unità di Pisa selezionerà e modellerà alcuni sistemi biologici; estenderà i formalismi usati; progetterà strumenti per la loro analisi e simulazione. Inoltre valideremo la nostra proposta mediante la simulazione di tali modelli, usando gli strumenti prototipali di cui disporremo.

Uno dei temi riguarderà lo sviluppo di un calcolo per descrivere cellule. Le sue primitive ispirate dalla biologia potrebbero aiutare a definire sistemi piú efficienti e affidabili di agenti di calcolo mobili e concorrenti. In particolare vorremmo primitive per descrivere sia reazioni biochimiche multiple e simultanee che il loro accadere in differenti siti e compartimenti delle cellule. Inoltre svilupperemo semantiche qualitative e quantitative, tipicamente stocastiche, per esprimere nozioni come causalità tra reazioni e reagenti, effetti catalizzanti/inibitenti e di concentrazione, descrizione di compartimenti e di membrane.

Realizzeremo un interprete per una variante stocastica del pi-calculus, sfruttando e migliorando l'algoritmo di Gillespie. L’interprete sarà equipaggiato con strumenti per estrarre dalle computazioni le informazioni utili ai biologi, p. e. concentrazione di una componente o frequenza di una interazione e sarà accoppiato con librerie statistiche per aiutare l'utente nella raccolta e nell'analisi dei dati degli esperimenti virtuali.

Per quanto riguarda l'attività di specifica, affineremo la descrizione di ViCe e procederemo con ulteriori simulazioni, con particolare attenzione all’emergere di comportamenti complessi. L’obbiettivo è di avvicinare il più possibile ViCe a un procariota reale, e a tal fine ViCe sarà arricchito dalla specifica di ulteriori vie metaboliche, in modo da realizzare una descrizione in silico di un microrganismo reale, quale Mycoplasma genitalium o Escherichia coli. Sperimenteremo in silico fenomeni perturbativi dell’equilibrio cellulare, quali il silenziamento genico o l’inibizione enzimatica. Inoltre, la simulazione in condizioni perturbate, permetterà di esaminare in silico la possibilità di attivazione di vie metaboliche alternative a quelle bloccate, e l’insorgenza di percorsi metabolici non esplicitamente descritti dalla biochimica classica.


Un secondo argomento di ricerca riguarda il Calculus of Looping Sequences (CLS). Lo arricchiremo con nozioni di tempo e probabilità, e con informazione quantitativa, p.e. per descrivere le velocità degli eventi come frequenze di applicazione di regole di riscrittura. Estenderemo perciò le bisimulazioni già definite per CLS.

Costruiremo uno strumento per simulare i sistemi descritti da CLS, usabile da biologi sia per spiegare che per predire comportamenti di processi biologici. Per validarlo, studieremo sistemi biologici reali, p.e. sistemi biologici in cui vi siano interazioni tra elementi sulle membrane cellulari.

Inoltre, estenderemo CLS con concetti topologici, per descrivere la posizione relativa dei siti dell’interazione , giacchè le interazioni avvengono soltanto tra cellule adiacenti. Anche in questo caso saranno sviluppati opportuni concetti di bisimulazione. Inoltre, intendiamo investigare quali tipi di proprietà verificabili mediante bisimulazione hanno una controparte rilevante nel mondo biologico.

Inoltre, ci proponiamo di ottenere analisi che verifichino proprietà temporali su computazioni piú generali di quelle classiche di safety, quali:
- per ciascun cammino “appena la molecola A reagisce con B, non interagirà piú con molecola C” oppure “la molecola A può apparire solo dopo la molecola B”;
- esiste un cammino in cui appare la molecola A.
La verifica di tali proprietà richiede analisi sí astratte, ma anche concrete per osservare i comportamenti di un sistema: esse dovrebbero correttamente approssimare il comportamento del sistema a tempo di esecuzione.

Infine estenderemo l’approccio di interpretazione astratta per trattare aspetti quantitativi e stocastici, in modo da fornire limiti inferiori e superiori su comportamenti stocastici.

Sede dell'Unità:  Università degli Studi di BOLOGNA

Compito dell'Unità

- Estensioni quantitative dei calcoli di processi biologici

La possibilità di avere a dispozione informazioni quantitative è cruciale nel campo dei processi biomolecolari, e quindi gioca un ruolo fondamentale anche nella modellazione dei sistemi biologici. La disponibilità di estensioni stocastiche risulta utile nella collaborazione con i biologi, i cui esperimenti si basano su valutazioni quantitative.

Svilupperemo estensioni stocastiche basate sui modelli stocastici attualmente disponibili. In particolare, intendiamo estendere i calcoli esistenti con aspetti probabilistici, utilizzando l'approccio seguito nello sviluppo del pi-calcolo stocastico.



- Analisi dell'espressività di calcoli di processi biologici e stocastici

Negli ultimi anni sono stati sviluppati svariati calcoli per processi biologici, ma non è ancora stato effettuato un confronto del potere espressivo di questi calcoli.
Ontendiamo studiare il potere espressivo di (frammenti e varianti) di calcoli di processi biologici.

Partendo dal lavoro iniziale del nostro gruppo sul confronto di varianti di Brane Calculi, nella prima fase estenderemo l'analisi ad altri calcoli.

I BioAmbients sono ottenuti adattando i Mobile Ambients al contesto biologico. Intendiamo adattare le tecniche che abbiamo sviluppato per l'analisi dell'espressività di vari frammenti e varianti di Mobile Ambients ai BioAmbients.

Intendiamo inoltre sviluppare un core calculus, che potrà essere utilizzato come una piattaforma comune per il confronto di calcoli di processi biologici.

La maggior parte del nostro lavoro sull'espressività è basato su risultati di separazione riguardanti la decidibilità o l'indecidibilità di proprietà quali la raggiungibilità, il deadlock, la divergenza, la boundedness, la coverability.
Questi risultati di decidibilità verranno utilizzati per ottenere tecniche di analisi per i sottocalcoli su cui le proprieta' risultano decidibili.
Si prevede di applicare tali tecniche di analisi anche a particolari classi di P systems.


- Modellazione e simulazione di processi biologici mediante sistemi a membrana

Intendiamo esaminare diversi fenomeni cellulari mediante l'applicazione dei sistemi a membrane. In particolare, i fenomeni che intendiamo analizzare sono:

1) L'attività dei canali meccanosensibili nei procarioti. La funzione svolta da questo tipo di canali consiste nel proteggere la cellula da valori eccessivi di pressione osmotica. La modellazione di questo tipo di canali permettera’ di definire qual è la probabilità di passare da una configurazione di un canale alla configurazione successive.

2) Oscillatori Bio-chimici. L'interazione tra due o piú sistemi oscillatori risulta essere molto importante per molti processi e sistemi biologici. Di fatto, costituisce un fattore importante per mantenere in vita un organismo o un sistema complesso costituito da diversi organismi. Riteniamo che i Sistemi a Membrane con priorita' che variano dinamicamente durante la computazione possano essere utilizzati con successo nello studio di queste dinamiche.

3) Canali di comunicazione cellulari, quali pompe sodio/potassio accoppiate, sistemi di antiporto per il sodio e il calcio e canali per la comunicazione di calcio. Lo studio integrato di tali canali di comunicazione potrebbe consentire di comprendere a fondo fenomeni importanti quali lo scambio di ioni a livello cellulare, che attualmente risultano essere chiari solo in alcuni aspetti.

4) Analisi del ruolo svolto dagli aminoacidi e dei loro derivati sul sistema nervoso. E' noto che vi sono diversi derivati degli aminoacidi che agiscono da eccitatori o inibitori in vari processi di comunicazione di segnali neurali. Un esempio di questo tipo e' rappresentato da un derivato degli aminoacidi noto come GABA, che agisce da inibitore nelle comunicazioni sinaptiche.

Prevediamo inoltre di sviluppare software di simulazione basati sul modello a Membrane.

Sede dell'Unità:  Università degli Studi di TRENTO

Compito dell'Unità

Gli obiettivi principali di questa unità di ricerca sono la definizione di un ambiente di specifica linguistico per le funzionalità dei sistemi biologici, la definizione di techniche di analisi di dati di espressione genica da microarray, la progettazione e sviluppo di prototipi per l'analisi di dati.

La ricerca sarà organizzata in due fasi. La funzionalità e il comportamento di sistemi biologici costituirà il dominio applicativo sia per la selezione di casi di studio appropriati (prima fase) che per la validazione finale dei modelli e dei prototipi sviluppati (seconda fase). I casi di studio andranno da semplici transcriptional circuits, metabolic pathways e signal transduction networks a modelli (semplificati) di sintesi di proteine a livello cellulare e modifica di conformazione della struttura di proteine. Prendendo spunto dai vari tipi di interazione rivelati dai casi di studio prescelti, raffineremo ed estenderemo alcuni precedenti lavori che usano i calcoli di processo per la modellazione di interazioni biochimiche e per la descrizione della evoluzione dinamica dei sistemi biologici. Questa attività consisterà principalmente nell'identificazione di primitive che tengano in considerazione gli aspetti intrinsecamente stocastici delle interazioni biologiche e permettano di definire un linguaggio ed una semantica operazionale che possa essere utilizzata come base formale per possibili successive automazioni. L'espressività del linguaggio sarà controllata verificando che sia possibile modellare, tramite i suoi termini, i vari scenari di interazione messi in luce dai casi di studio. Per ciò che riguarda la ricerca relativa all’analisi di dati, si individueranno gli obiettivi dell'analisi (e.g., diagnostico, esplorativo, confermativo) e un sottosistema biologico per cui siano disponibili dati di microarray compatibili con gli obiettivi prescelti.

Nella seconda fase del progetto procederemo alla validazione del linguaggio modellando i casi di studio selezionati. Verrà inoltre definita una tecnica di analisi di dati che sfrutti il risultato delle simulazioni nelle comuni operazioni di analisi (e.g., controllo di qualità). Si realizzeranno prototipi per l’implementazione della suddetta tecnica e per l’analisi comportamentale di processi del linguaggio di specifica. Studieremo anche possibili definizioni di equivalenze comportamentali ispirate alla biologia e a comportamenti di tipo stocastico. Le equivalenze comportamentali sono state abbondantemente approfondite nell'area della semantica per la concorrenza: due sistemi si dicono equivalenti quando, immersi in un qualunque contesto (cioè utilizzati come componenti di sistemi di maggiori dimensioni), non è possibile osservare alcuna differenza tra i loro comportamenti. Per analogia al caso dei sistemi distribuiti, si potrebbe ad esempio pensare che due molecole sono equivalenti quando, in presenza degli stessi complessi molecolari, danno luogo alle stesse reazioni biochimiche, cosí come avviene per gli anticorpi o per qualche fattore di trascrizione. La definizione di equivalenze appropriate, permettendo la minimizzazione del numero di stati corrispondenti al comportamento (transition system) dei processi, sarà uno strumento particolarmente utile all’automazione dell’analisi del comportamento dei sistemi descritti.

Sede dell'Unità:  Università degli Studi di SIENA

Compito dell'Unità

Recentemente è stato sviluppato un modello in Pi-calculus di un procariota minimale. Il modello è stato implementato ed è iniziata una fase sperimentale di verifica del modello.
L’eventuale ulteriore corrispondenza dei comportamenti in silico con omologhe osservazioni in vivo potrebbe rappresentare una conferma decisiva della validità del modello, ed aprire la strada all’utilizzo della “cellula virtuale” a scopo predittivo.

Per il modello di base sviluppato non sono ancora state definite tecniche formali di verifica delle proprietà del sistema corrispondente, inoltre sono necessarie estensioni del modello per poter caratterizzare l'evoluzione temporale del comportamento, essenziale per molti sistemi biologici. Modelli informatici che risultano adatti alla descrizione di questi aspetti del comportamento dei sistemi biologici sono i cosiddetti sistemi real-time.
Questi sistemi interagiscono costantemente con l'ambiente e devono rispettare precisi vincoli temporali, sia di tipo qualitativo che di tipo quantitativo. In questi sistemi l'evoluzione temporale gioca un ruolo primario, evidenziato dal fatto che la violazione di un vincolo può avere ripercussioni disastrose sul sistema e sull'ambiente in cui il sistema agisce. Proprio a causa dell'importanza che l'evoluzione temporale ha in un sistema real-time, accanto allo sviluppo di vari formalismi per la descrizione di questi, il problema della verifica delle proprietà di un sistema real-time è particolarmente rilevante e necessita di strumenti adeguati. Negli ultimi anni l'interesse per modelli che possono descrivere e specificare sistemi real-time è notevolmente aumentato. Si sono sviluppati così diversi formalismi per arricchire la logica temporale e per catturare più precisamente lo scorrere del tempo fisico. Nell'ambito dei modelli e logiche per sistemi real-time l'unità di Siena si è occupata di tecniche di specifica, verifica e di sistemi di prova. Queste tecniche sono tuttavia state sviluppate prevalentemente per sistemi informatici. Nell'ambito del progetto vogliamo estendere sia le tecniche di model-checking, che i sistemi di prova per logiche temporali per alcuni dei modelli di sistemi biologici definiti nel progetto.

Un altro ambito di ricerca su cui intendiamo lavorare riguarda la definizione di modelli basati su tecniche di machine learning e algoritmi genetici per analizzare dati di genomica strutturale. Verranno perseguiti i seguenti obiettivi: lo sviluppo di paradigmi adattativi, ovvero di natura probabilistica, capaci di realizzare inferenze di natura strutturale a partire dall'informazione incapsulata a livello di sequenze e l’analisi/inferenza automatica a partire da dati relativi a esperimenti con array-CGH su DNA.