RICERCA ITALIANA     

Programma di ricerca

Systems Biology: modellazione, linguaggi e analisi (Sybilla)

Università di riferimento

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

Responsabile dell'Unità di ricerca

Alberto POLICRITI

Descrizione

La teoria dei processi biochimici cerca di creare un contesto unificante in cui ragionare sui percorsi biochimici e sui processi evolutivi che li hanno plasmati. Ci sono molte componenti interrelate. Queste includono modelli derivati dalla cinetica massa-azione che si focalizza sulle concentrazioni di sostanze chimiche; modelli derivati da eventi discreti come la specializzazione, la differenziazione e l'auto-rinnovamento; modelli derivati dai segnali cellulari; modelli derivati da grandi popolazioni cellulari; e modelli che considerano la compartimentazione cellulare ed il trasporto attraverso membrane e tra compartimenti. Le richieste che questi modelli impongono sulla tecnologia dell'informazione vanno ben al di la' dell'area biologica; questa unita' indirizzera' varie questioni correlate con aspetti numerici, probabilistici, logici e simbolici della computazione e, in particolare, come essi possono essere implementati sulle moderne architetture computazionali. Intendiamo principalmente considerare le seguenti aree di ricerca che sono tra loro strettamente correlate. (a) Modelli: Automi, Logiche Temporali e Tecniche di Riduzione. Sebbene i processi biochimici possano essere rappresentati in forma compatta come sistemi di ODE (Ordinary Differential Equations) o SDE (Stochastic Differential Equations), tali rappresentazioni sono piuttosto inadatte ed inefficienti per ragionare. Approcci tradizionali basati sull'integrazione numerica e la simulazione, falliscono rapidamente l'obiettivo di fornire le intuizioni rilevanti anche per sistemi ragionevolmente complessi. Pensiamo che gli automi (sia discreti che ibridi) possano modellare praticamente ed elegantemente tutti i meccanismi di controllo biologico, ci permettano di ragionare su tali meccanismi in sistemi di Logica Temporale, e possano diventare il contesto fondazionale per il campo emergente della system biology. Tali modelli, grazie all'applicazione di gia' note tecniche di riduzione, consentono un'analisi piu' rigorosa di grosse quantita' di dati biologici, prodotti come tracce (numeriche) di esperimenti in vivo, in vitro e in silico -- attualmente attivita' centrale di molti biologi e biochimici. (b) Ragionamento ed Estrapolazione: Tecniche di Computazione Simbolica. La rappresentazione ed il processo di riduzione di automi forniscono rappresentazioni efficienti, ma gli algoritmi di ragionamento su questi modelli possono essere inefficienti e male adattabili al crescere delle dimensioni. Algoritmi basati sulla manipolazione simbolica di formule possono garantire significativi miglioramenti nella complessita' computazionale. Inoltre, le tecniche di manipolazione simbolica, sotto opportuni vincoli, permettono di costruire una rappresentazione contenente piu' informazioni di una simulazione puramente numerica del sistema, e suggeriscono intervalli di variazione per i parametri del modello e punti critici per lo spazio degli stati. MODELLI: AUTOMI, LOGICHE TEMPORALI E TECNICHE DI RIDUZIONE Intendiamo disegnare uno strumento capace di usare sia dati utili per una modellazione matematica "classica" che, quando disponibili, informazioni sui meccanismi di controllo soggiacenti al sistema. In altre parole, intendiamo combinare le due, in qualche modo, separate tradizioni in una singola cornice, deducendo la struttura dell'automa da (1) dati sperimentali e (2) traiettorie derivate da modelli matematici. Per questo obiettivo, abbiamo bisogno di descrivere la semantica di un sistema usando un automa che catturi le caratteristiche qualitative del sistema biologico. Una via possibile, parzialmente analizzata in [37,46,47], per costruire l'automa e' la seguente: istantanee delle variabili di sistema costituiscono l'insieme dei possibili stati dell'automa. Le transizioni sono dedotte dalla evoluzione delle tracce delle variabili di sistema. Gli stati finali sono quegli stati in cui la simulazione raggiunge una fine riconoscibile e si suppone siano punti di equilibrio per il percorso metabolico oggetto di studio. Gli automi possono essere arricchiti con etichette su nodi e/o archi che permettono di mantenere informazioni relative alle proprieta' dei nodi e di imporre condizioni sulle azioni rappresentate dagli archi. Intendiamo analizzare quali automi meglio si prestino a rappresentare diversi sistemi biologici (automi standard, con etichette su nodi/archi, automi ibridi). Testare se il sistema biologico modellato attraverso un automa soddisfi o meno una data proprieta' P e' equivalente a testare se l'automa soddisfa la formula della logica temporale che codifica P. Un esempio semplice e naturale di proprieta' logica di molti sistemi biologici e' la nozione di "steady state", il sistema resta "fisso" al passare del tempo. Un'altra proprieta' naturale riguarda la limitatezza delle concentrazioni di reagenti coinvolti in processi biologici e puo' essere necessario accertarla come precondizione ad altre proprieta' quali l'esistenza di un ciclo limite, soluzioni a stabilita' multipla, meta-stabilita', o isteresi. Usando una logica temporale proposizionale e basandosi sulle nozioni di model-checking si puo' analizzare una o piu' tracce dell'automa, dove la singola traccia e' creata da un singolo "set-up" (e.g. condizioni iniziali, un insieme di valori per i parametri, un insieme di segnali di eventi, ecc.) del sistema oggetto di analisi. Basilare e' il fatto che la logica temporale permetta di specificare chiaramente il significato di termini tempo-dipendenti del linguaggio naturale, quali "prima o poi" e "sempre", in relazione al comportamento astratto del sistema in discorso. Come esempio, si consideri la seguente frase: "La concentrazione di guanosine triphosphate (GTP) e' uguale ad X". Dato un sistema biologico in equilibrio, la frase precedente puo' essere vera in alcuni o nessuno degli istanti temporali. In particolare, possiamo facilmente costruire enunciati (in un opportuno linguaggio naturale) che esprimono il fatto che, dato un certo insieme di condizioni iniziali, l'enunciato di cui sopra sara' vero "eventually". La logica temporale formalizza precisamente il significato del termine "eventually" (e quello di altri "modi": "always", "infinitely often" e "almost always"), e la semantica risultante conduce ad un algoritmo di model-checking per determinare la validita' di enunciati di logica temporale nel contesto dei nostri automi (si veda [37,46,47]). Logiche temporali opportunamente arricchite permettono anche di analizzare proprieta' dinamiche dei processi biologici e di "riunire" componenti diverse del sistema che possono essere co-regolate o anti-regolate. Intendiamo analizzare quali logiche temporali meglio si adattino a studiare proprieta' biologiche interessanti e sviluppare relativamente a tali logiche ed agli automi utilizzati per la modellazione algoritmi efficienti di model checking. Un punto focale nella nostra ricerca e' la questione di tenere sotto controllo la complessita' degli automi mediante "collassi" simbolici, e rappresentazione modulare dei modelli. Cio' permette lo studio parallelo di molte evoluzioni ed esperimenti che differiscono per costanti di proporzionalita' dei cambiamenti e di ordini cinetici (in una singola struttura). Nei casi pratici, gli automi costruiti a partire dalle tracce hanno un numero di stati enorme. Abbiamo esplorato due tecniche per ridurre il numero degli stati di automa, cioe' la proiezione ed il collasso (si veda [37,46,47]). Per evitare approssimazioni dei risultati dovuti all'uso di collasso e proiezione, e per ottenere un metodo piu' potente e flessibile, e' stato introdotto in [6] l'uso di automi ibridi insieme con una riformulazione della proiezione e del collasso. Intendiamo analizzare l'utilizzo di altre tecniche di riduzione dei modelli derivanti dal model checking (per esempio bisimulazioni) che devono essere opportunamente adattate dipendentemente dalla logica temporale di interrogazione. La simulazione, numerica o simbolica, gioca un ruolo chiave in ogni aspetto di questo progetto. Tradizionalmente, la simulazione numerica con la successione di passi di un integratore, o la simulazione stocastica con una sequenza di eventi reagenti, hanno costituito il motore computazionale di base per rispondere a molte questioni scientifiche relative a come predire un risultato osservando un modello di sistema in evoluzione. Ci sono molte trappole inerenti a questi approcci: la violazione delle leggi di conservazione causata dagli errori numerici, l'instabilita' numerica introdotta da riduzioni di modello inappropriate, la perdita di fedelta' o di efficienza nel simulare un modello che prevede molte scale temporali diverse, ecc.. Possiamo alleviare questi problemi essenzialmente facendo uso di una "aritmetica esatta" disponibile tramite la simulazione simbolica e introducendo vincoli ed invarianti. Tuttavia, c'e' un punto in cui la simulazione riemerge come una componente critica del nostro contesto: cioe', nel tentativo di spiegare una ipotesi falsificata mediante la simulazione di controesempi. Data la natura ed il potenziale del nostro sistema, ogni specifico enunciato logico temporale viene verificato a livelli di astrazione multipli in automi ibridi molto distanti dal modello fisico di base (e.g. quello piu' prossimo al livello delle interazioni molecolari o cellulari). Quindi, se un enunciato specifico e' determinato essere falso in uno dei nostri modelli, deve essere spiegato mediante un controesempio nel nostro caso una traccia di eventi rappresentanti le interazioni. Una simulazione di tal guisa deve essere consistente con i livelli piu' alti di astrazione e le scelte dei parametri ad ogni livello di astrazione, e puo' coinvolgere molti orologi ognuno dei quali avanza ad un ritmo diverso. Quindi, avremo bisogno di sviluppare strumenti di simulazione di base che usino tecniche numeriche, multi-scala, event-driven, "tau-leaping" e astraibili mentre, allo stesso tempo, saranno vincolati da invarianti e astrazioni multiple. Riassumendo le questioni che intendiamo esplorare sono: - Sistemi di interrogazione: se un biologo vuol ragionare su un sistema mediante interrogazioni logiche formulate in un opportuno query language (e.g. la logica temporale), quali sono i migliori query languages? Quali sono i migliori algoritmi che siano in grado di avvantaggiarsi delle strutture simboliche? Quali sono le strade corrette per risolvere i problemi associati con (a) equivalenza di modello, (b) analisi sperimentale e (c) analisi di raggiungibilita'? - Sistemi ibridi: certe interazioni sono puramente discrete e dopo una tale interazione la dinamica del sistema puo' cambiare. Per un modello ibrido di questo tipo l'automa soggiacente deve essere modificato per un tale "mode". Questi rafforzamenti espressivi come modificano il modello di base? - Spazio degli stati (Spazio prodotto): l'interazione di un gruppo di cellule puo' essere modellata mediante il prodotto di automi. Oltre al classico problema dell'esplosione esponenziale degli stati, dobbiamo anche stare attenti alla struttura delle variabili correlata con (a) divisione cellulare, (b) apoptosi e (c) differenziazione. RAGIONAMENTO ED ESTRAPOLAZIONE: TECNICHE DI COMPUTAZIONE SIMBOLICA Gli automi ibridi sopra menzionati approssimano complicati sistemi biochimici non lineari in termini di un modello che e' in parte discreto ed in parte continuo. Quando il sistema e' in un particolare stato discreto (spesso definito "control mode"), evolve nel suo stato continuo descritto mediante un sistema dinamico. Le transizioni (spesso chiamate "control switches") dell'automa discreto hanno luogo (magari probabilisticamente) quando lo stato continuo del sistema soddisfa certe condizioni di guardia. Cosi' come si ragiona nel contesto di sistemi ingegnerizzati in modo complesso (sistemi di controllo, sistemi digitali, protocolli di comunicazione, ecc.), nelle applicazioni relative alla biologia abbiamo anche bisogno di risolvere "safety", raggiungibilita', "liveness" e altre interrogazioni complicate coinvolgenti quantificazioni di ordine superiore. Molte forme di enunciati in logica temporale possono essere usate per esprimere interrogazioni di questo tipo ma queste possono non produrre soluzioni algoritmicamente efficienti. Intendiamo investigare approcci "algorithmic algebraic" che si generalizzano anche ad una piu' ampia classe di sistemi (cf. [13, 18, 25]), e che si collegano a molti problemi matematici irrisolti ed interessanti. Inizieremo studiando una metodologia per risolvere il problema del model checking per logiche temporali in automi ibridi in cui gli insiemi e le relazioni rilevanti sono semi-algebrici. L'approccio generalizza ad altre logiche temporali e versioni di logiche dinamiche. Dato un modello ibrido M e una formula p nella logica di nostra scelta, cerchiamo di computare una relazione di derivabilita' che corrisponde a "p e' vera in M a partire da X e all'istante t", dove X e' uno stato continuo che denota lo stato di partenza e t e' la variabile temporale. La maggior parte dei problemi qui sono di natura matematica e tecnica. Crediamo che ci siano una quantita' di tecniche recentemente sviluppate dalla comunita' della computazione simbolica che possono essere utilizzate in questo contesto. L'obiettivo principale della nostra ricerca rimane comunque la creazione di una chiara, generale, unificante, "model-based", sistematica e rigorosa metodologia, che tenga aperta la strada per modelli di grossa scala, complessi e spazio-temporali. Alcuni dei problemi sono: (1) La creazione di una metodologia unificante che sussuma precedenti tecniche simboliche basate su OBDD o piu' recenti tecniche SAT-based. Queste generalizzazioni naturali richiedono la codifica semialgebrica di transizioni ed il successivo collegamento con il Positivestellensatz. (2) La generalizzazione di automi ibridi oltre i lineari e rettangolari sui quali si possa ragionare efficientemente. (3) La costruzione di algoritmi piu' efficienti che possano usare tecniche randomizzate o probabilistiche (permettendo risposte "non so"). Intendiamo inoltre studiare l'applicazione di tecniche simboliche analoghe a quelle sopra menzionate, per il problema di predizione del folding di una proteina. Per tale problema non esistono allo stato attuale algoritmi con approssimazione ed efficienza soddisfacente. Si desidera studiare la modellizzazione del processo di folding di una proteina. Saranno studiati sia modelli discreti (a reticolo) che continui e con diverso livello di granularità (aminoacido/atomico). Saranno descritti simulatori codificati in linguaggi concorrenti e in automi ibridi. Saranno combinati con risultati dello studio del problema basati su minimizzazione di funzioni in programmazione con vincoli. L'obiettivo che ci si pone è riuscire a predire mediante simulazione e analisi di proprietà di linguaggi formali i vari segmenti di struttura secondaria di una proteina. In un secondo tempo, sia mediante simulazione che programmazione con vincoli predire la struttura nativa (ed il processo di folding) per proteine di lunghezza vicina ai 100 aminoacidi.