RICERCA ITALIANA     

Systems Biology: modellazione, linguaggi e analisi (Sybilla)

Università degli Studi di Trento

Abstract

Pianifichiamo di determinare tecniche e modelli (sia a livello linguistico testuale che grafico) di sistemi biologici complessi. Doteremo i nostri formalismi con strumenti di analisi del comportamento dinamico e della evoluzione temporale dei sistemi considerati riusando il più possibile i risultati della teoria della concorrenza e dei linguaggi formali. Utilizzeremo in questo progetto anche risultati dall'area della simulazione includendo informazioni quantitative nelle specifiche dei casi di studio. Infine investigheremo come i formalismi logici possono essere usati e adattai al nuovo dominio applicativo biologico.

Lo sviluppo descritto sopra è poi adattato, verificato e validato mediante casi di studio provenienti dalla letteratura e dall'interazione con gruppi biologici che ogni unità coinvolta nel progetto ha in altri progetti.

La fattibilità dell'approccio è mostrata realizzando srtumenti proof-of-concept basati sui framework teorici sviluppati nella prima fase di investigazione.

Il focus principale delle attività svolte è sull'informatica poichè si produrranno nuove primitive di calcoli e nuovi strumenti software di analisi che saranno poi istanziati al dominio biologico. Il positivo effetto collaterale di questa ricerca è che nuovi paradigmi computazionali potrebbero emergere prendendo ispirazione dal modo in cui la materia vivente manipola l'informazione. <<<

Coordinatore Scientifico del Programma di Ricerca

Corrado PRIAMI Università degli Studi di TRENTO

Obiettivo del Programma di Ricerca

L'obiettivo ultimo della biologia dei sistemi è predirre il comportamento della materia vivente. Se noi possiamo determinare delle tecniche che ci consentono di modellare sistemi biologici per poi potereli analizzare e simulare siamo sulla giusta strada. In ultima analisi vogliamo comprendere il funzionamento delle cellule ad un giusto livello di aastrazione e vogliamo avere modelli che ci consentano di predirre dei comportamenti sconosciuti. Questi risultati ci consentirebbero di usare materia biologica come un flessibile strumento di manipolazione di informazione e quindi di calcolo. <<<

Risultati parziali attesi

I risultati parziali attesi da questa fase sono:

- definizione di nuove primitive per modellare sistemi biologici mediante algebre di processo e loro estensione stocastica per gestire parametri quantitativi;

- nuovi modelli basati su automi ibridi e su logiche temporali ispirati dalla biologia;

- Estensione dei sistemi a membrane con probabilità per definire modelli di interazione insistemi biologici;I risultati attesi sono:

- generalizzazione degli automi ibridi e definizione di algoritmi efficienti per analizzare proprietà di sistemi biologici;

- definizione di strumenti di simulazione per sistemi ibridi, algebre di processo e sistemi a membrane;

- nuove tecniche per affrontare il problema del protein folding;

- riuso di strumenti esistenti per verificare modelli di sistemi biologici specifiacti mediante logiche;

- influenza reciproca dell'area della sicurezza informatica e modelli biologici , ad esempio del sistema immunitario;I risultati attesi sono:

- modellazione e analisi di sistemi biologici per per sintonizzare e validare le idee e gli strumenti proposti nelle altre fasi; <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

Uno dei problemi della biologia contemporanea consiste nella comprensione della dinamica dei geni e delle proteine all'interno delle cellule, quando danno origine ad un organismo vivente [Kitano02]. Sfortunatamente, non esistono tecniche sperimentali in grado di tracciare la dinamica del completo metaboloma di una cellula. Un approccio promettente è la rappresentazione delle relazioni conosciute tra elementi in un metaboloma virtuale, che porta ad una sorta di cellula virtuale [LS01]. Esistono numerose proposte di modellazione biochimica [GP98,DL03,NOMK99]. Qui, ci concentriamo sui metodi formali. Faremo una breve rassegna su quegli approcci che sfruttano le analogie tra le reti di cellule biochimiche e le reti di processi che eseguono calcoli.

Una rete di biocellule può essere vista come una macchina in grado di calcolare, composta di agenti di elaborazione che interagiscono e cooperano per raggiungere un obiettivo comune. Gli agenti calcolano autonomamente in modo indipendente e scambiano informazione tra di loro [RS02]. Questa descrizione informale si applica allo stesso modo ai sistemi concorrenti, nel cosí detto campo del "global computing". Questi sistemi sono composti da un largo numero di agenti di calcolo che possono essere mobili e comunicare tra loro, e che sono distribuiti geograficamente. È quindi naturale cercare di trasferire le tecniche prese dal campo del global computing per studiare il comportamento delle cellule
biologiche. Promettente è l'uso di calcoli di processo, ovvero di formalismi usati per la descrizione di sistemi mobili e distribuiti. I calcoli di processo sono matematicamente ben fondati e sono dotati di strumenti per l'analisi statica e dinamica. Questi stessi strumenti di analisi possono dunque essere utilizzati anche nel caso degli organismi biologici. Uno dei primi esempi di un calcolo per modellare sistemi biochimici atttraverso un calcolo è stato il lavoro di Fontana e Buss [FB96], nel quale si utilizza una versione del lambda-calculus. Una migliore descrizione dei percorsi biologici è stata proposta da Regev, Silverman e Shapiro [RSS01], che usano a questo scopo il pi-calculus [MPW92], noto formalismo per la mobilità. Poi Priami, Regev, Silverman e Shapiro arrichiscono in [PRSS01] il pi-calculus considerando aspetti quantitativi e sfruttandone una variante stocastica, originariamente proposta da Priami in [Priami95], per valutare le prestazioni dei processi concurrenti e mobili. Curti, Degano, Priami e Baldari usano invece una semantica arricchita ("enhanced ") del pi-calculus in [CDPB04] allo scopo di rappresentare gli aspetti del comportamento dei processi legati alla causalità e alla località, migliorando in questo modo l'espressività delle specifiche e consentendo al tempo stesso la rappresentazione grafica delle computazioni. Questa versione arrichita del pi-calculus è alla base anche della specifica e dell'analisi, in [CCDM], di un'ipotetica cellula con un genoma il più basilare possibile. Questo procariota virtuale presenta in simulazione un comportamento simile a quello di procarioti reali, il che convalida la specifica degli autori. Tra i vari calcoli usati nella System Biology, menzioniamo anche il Bio-calculus proposto da Nagasaki, Onami, Miyano e Kitano in [NOMK99], un ambiente che include un editore di equazioni, un interprete e un'interfaccia grafica e i cui utenti descrivono i percorsi usando le convenzionali equazioni biochimiche.
Recentemente, Regev ha proposto Bio-ambients [Reg03], una variante dell' Ambient Calculi [CG98] di Cardelli e Gordon, dove i compartimenti sono descritti come una gerarchia di ambienti dotati di confini. Questa gerarchia può essere modificate grazie ad
opportune operazioni che hanno un'immediata interpretazione biologica. Ad esempio, le interazioni tra i composti che risiedono all'interno del "cytosol" e del nucleo sono rappresentati attraverso comunicazioni di tipo padre-figlio, sfruttando la nozione di
compartimento. Danos e Laneve [DL03] hanno recentemente proposto il Core Formal
Molecular Biology, partendo dalle primitive basilari del pi-calculus. Come negli altri modelli basati sul linguaggio a cui abbiamo fatto cenno sopra, i processi rappresentano i composti, l'insieme dei processi rappresenta invece le soluzioni, e il loro comportamento viene dato da un insieme di regole di riscrittura che spiegano ad esempio l'attivazione, la sintesi e la complessazione. Le Reti di Petri (Petri Nets) sono un altro formalismo usato per modellare i sistemi concorrenti. Essenzialmente, si tratta di automi i cui stati sono insiemi di componenti distribuiti, e le cui transizioni trasformano solo alcuni elementi di uno stato. Varianti di Reti di Petri sono state largamente usate nella System Biology [GP98,HT98,KL91], anche grazie alla loro intuitiva rappresentazione grafica; come prevedibile, le piazze rapprestano molecole, mentre le transizioni rappresentano le reazioni. In [RLM96], Place/Transition Petri Nets sono utilizzate per l'analisi quantitativa dei processi biochimici. Di recente,in [HKW03] si è fatto uso di una semantica del formalismo per decidere sulla coerenza dei modelli. Self-modified Petri Nets sono state usate invece per rappresentare un modello quantitativo delle reti biochimiche [HT98], mentre le Hybrid Petri Nets [MDNM00] hanno modellato le reti regolatorie prendendo in considerazione concentrazioni di proteine e RNA. Le Stochastic Activity Networks estendono le Reti di Petri, e vengono utilizzate in [ML97] per la rappresentazione dei percorsi biologici e per la simulazione della loro cinetica. MetaNets [KL91] rappresenta invece un modello delle reti metaboliche espressione di geni. Facciamo cenno anche ad alcuni recenti approcci basati sugli "statecharts" che forniscono un modello quantitativo dei sistemi cellulari con componenti molecolari [HB98,KCH02]. Tra i vari strumenti per l'analisi dinamica dei processi si possono trovare gli "workbench" per la concorrenza e la mobilità, basati sulla semantica predisposti per la manipolazione e l'analisi dinamica dei sistemi mobili e concorrenti. Sono infatti in grado di effettuare varie analisi dei comportamenti dei processi, specificati usando calcoli di processo, come ad esempio l'analisi dello spazio degli stati o il controllo di varie equivalenze semantiche e di preordini. Si possono trovare anche strumenti simili per l'analisi dei sistemi descritti in termini di un modello stocastico. Un esempio è dato dall'workbench PEPA, dove il modello è dato nell'algebra di processi PEPA. Un altro è BIO-SPI [PRSS01]. Un altro esempio è dato invece da TwoTowers, uno strumento software per la verifica funzionale e la valutazione dei sistemi di computer, di comunicazione e software, modellati attraverso algebre di processo stocastiche. Recenti risultati incoraggianti sono stati ottenuti dall'uso di una particolare tecnica statica, detta Analisi di Flusso di Controllo, per la convalida di proprietà di sicurezza per i sistemi concorrenti e mobili [BDNN01ic]. Come altre tecniche statiche, l'Analisi di Flusso di Controllo offre un repertorio di metodi e strumenti automatici e decidibili per l'analisi di proprietà di sistema. Si spera che questi strumenti possano essere sfruttati anche per analizzare i processi offerti alla modellazione dei sistemi biologici.


I Sistemi a Membrane sono modelli di calcolo legati all'area del calcolo molecolare, recentemente introdotti da G. Paun. Il modello trae spunto dall'osservazione che i processi e le reazioni chimiche che avvengono a livello cellulare possono essere considerati come processi di calcolo. Qualunque sistema biologico non elementare e' costituito da diverse componenti, ognuna delle quali svolge processi informativi differenti e comunica i propri risultati alle altre. Ogni componente e' delimitata da un diverso tipo di membrana, che funge da separatore e da barriera semi-permeabile, che assicura il passaggio selettivo di alcune sostanze e ne blocca altre. Per definire una controparte formale della cellula, è necessario definire, pertanto, una struttura che tenga in considerazione l'architettura gerarchica che costituisce una cellula. Tale struttura è definita "Struttura a membrane" e consiste di un insieme di membrane ordinate secondo una precisa gerarchia e contenute in una membrana principale (skin/pelle) che separa l'intero sistema dall'ambiente esterno. All'interno delle varie regioni definite dalle membrane, possiamo considerare insiemi di oggetti e regole di evoluzione. Tali regole di evoluzione agiscono non soltanto sugli oggetti, modificandoli e comunicandoli tra le diverse regioni attraverso le membrane, ma anche sulle membrane stesse, creandole, dissolvendole o dividendole. Il modello di computazione in tal modo ottenuto e' detto Sistema a Membrane (P sistema). Partendo da una configurazione iniziale (con diversi oggetti nelle diverse regioni), il sistema evolve fino a raggiungere, eventualmente, uno stato in cui non e' piu' possibile applicare alcuna regola di evoluzione. Il risultato della computazione è costituito dagli oggetti presenti in una particolare regione oppure, in alternativa, dagli oggetti espulsi attraverso la membrana piu' esterna. Una delle caratteristiche piu' interessanti di questi sistemi riguarda il grado di parallelismo che si ottiene: tutti gli oggetti che possono essere modificati, tramite l'utilizzo di una regola, vengono modificati contemporaneamente. Inoltre, tutte le componenti che fanno parte del sistema lavorano in parallelo [A8]. Un altro aspetto molto importante di questo tipo di sistemi riguarda la loro definizione che, come detto, trae spunto dal funzionamento della cellula. E' pertanto naturale pensare all'utilizzo di tali sistemi per definire modelli relativi a processi biologici di vario tipo, cosi' da poter acquisire informazioni che possono rivelarsi molto utili per i biologi. Alcuni passi iniziali in questa direzione sono già stati fatti: in [A11] sono stati presi in considerazione aspetti energetici legati alle reazioni cellulari; in [A15] si è considerato un modello formale per descrivere la fotosintesi; le comunicazioni che avvengono a livello cellulare sono state oggetto di studio in [A5]; infine, in [A1,A4,A14,A22,A25] si sono analizzati aspetti diversi legati a organismi e sistemi biologici di vario tipo.

Alla fine degli anni settanta, la comunita' di Intelligenza Artificiale ha sviluppato sistemi come Mycin e vari database di percorsi metabolici quali BioCyc, KEGG, PathDB, WIT, ecc.. Gli attuali sistemi in quest'area si concentrano sul rappresentare gli aspetti descrittivi dei percorsi metabolici e regolatori, delle reti di geni, o delle interazioni proteina-proteina. Approcci piu' quantitativi, concentrati sulla modellazione di sistemi biologici, sono stati sviluppati, particolarmente importante tra essi il lavoro di Voit e Savageau [44] e quello di Tyson e Novak [41]. Gli approcci basati sulla simlazione spaziano dal lavoro di Gillespie [16] negli anni settanta, fino al piu' recente System Bilogy Workbench (con il formato XML di scambio denominato SBML), a molti componenti del sistema BioSpice, al sistema E-CELL [39], al virtual Cell [36] e a GEPASI. Strumenti di ragionamento basati su algebra simbolica, logica temporale, e approcci basati su controllo appartengono ad una quarta classe di ricerche. Questi strumenti sono da poco stati considerati come utilizzabili per gli obiettivi che abbiamo descritto e, al meglio della nostra conoscenza, non sono ancora nel vocabolario comune dei sistemisti di modelli biologici. Durante la meta' degli anni novanta e successivamente, e' nato un crescente interesse nei Sistemi ibridi sia nel campo dell'Informatica che in quello dell'Ingegneria. Questo crescente interesse e' nato dalla necessita' di riconciliare il corpo delle conoscenze sui sistemi discreti e sui sistemi continui. In sostanza, un Sistema ibrido e' semplicemente un Automa a stati finiti (Finite State Automaton, FSA), dove ogni stato ha associato un insieme di equazioni differenziali (algebriche). In altre parole, un sistema ibrido è semplicemente una descrizione di un sistema (biologico) in cui certi modi discreti di comportamento vengono riconosciuti. Il comportamento del sistema all'interno di ogni modo e' modellato da un sistema di equazioni differenziali e le trasizioni di modo sono descritte da condizioni vero/falso, insieme con indicazioni di "change" degli osservabili sottostanti. I "modi" sono chiamati anche stati e le "condizioni" sono anche chiamate
guardie. Molti sistemi biologici possono essere modellati mediante sistemi ibridi. Per esempio, nel Ciclo cellulare il dimezzamento delle masse delle cellule dopo una divisione cellulare-una transizione tra due modi operativi-e' uno dei "cambiamenti" discreti e discontinui delle variabili osservabili. La capacita' di un sistema ibrido di rappresentare percorsi regolatori, dove repressione o inibizione di un gene cambia il comportamento di un insieme di percorsi metabolici, e' la particolare caratteristica che li rende attraenti come strumento per modellare sistemi bio-molecolari [1]. In [5, 14, 42] sono stati implementati simulatori e analizzatori di sistemi ibridi. Inoltre, sono stati sviluppati linguaggi in grado di codificare sia sistemi ibridi che altri sistemi simili in cui la struttura
temporale e di sincronizzazione sottostante e' un misto di transizioni sincrone e asincrone. Questi linguaggi sono espressivi ed intuitivi al punto da garantire ad un utente non matematico di comunicare rigorosamente e fedelmente la struttura di un sistema biologico senza sforzo. Nella maggior parte dei casi, siamo interessati alla verifica di
proprieta'; per esempio, safety--la concentrazione di una proteina P non superera' mai le X µMol--una proprieta' di raggiungibilita', oppure liveness--la concentrazione di mRNA R oscillera' sempre tra a e b. Per controllare queste proprieta' dei sistemi discreti (safety, liveness, ecc.) adoperiamo alcuni strumenti e tecniche. Model Checking e strumenti di dimostrazione automatica basati su automi e/o logica temporale si sono risultati estremamente utili nel contesto della verifica dell'hardware e del software. Essenzialmente, tutti questi strumenti eseguono varie forme di analisi di raggiungibilita' sullo spazio degli stati, la cui dimensione puo' risultare esponenziale nel numero di componenti. Sistemi attuali come smv e NuSMV, SyMP, e Kronos forniscono una cornice per molti
possibili sviluppi. Per esempio, Kronos e' usato per testare specifiche di automi temporizzati-una caratteristica che è molto importante per il nostro progetto. Questa classe di strumenti e' comunemente usata come una specie di "debugger" per hardware, software e modelli di sistemi di comunicazione. Nella modellazione di sistemi
biologici, essi potrebbero fornire informazioni utili per disegnare esperimenti "wet" di laboratorio. Strumenti per verificare proprieta' di sistemi ibridi risultano in genere piu' complessi. I sistemi allo stato dell'arte trattano solo con tipi ristretti di sistemi ibridi, i cosiddetti sistemi ibridi lineari o rettangolari, usando un quoziente
dello spazio degli stati e impiegando tecniche di bisimulazione per verificare proprieta' di safety e di liveness. HyTech proveniente dall'Universita' di Berkeley e' un esempio di tali sistemi. Il nostro lavoro sul collassamento e la bisimulazione [6] semplifica l'applicazione volta alla verifica di proprieta' per sistemi ibridi nel nostro contesto. Naturalmente, tali considerazioni giocano un ruolo importante quando si tratta con questioni di
composizionalita' di modelli; esploreremo queste questioni nella nostra cornice generale [3, 10, 12, 32]. Sebbene il model checking sia stato usato con successo per provare proprieta' di sistemi discreti ed ibridi, in specifiche applicazioni l'esplosione dello spazio degli stati rende il model checking non efficiente. In questi casi la scelta ricade su strumenti basati sul teorem proving [31]. <<<