Contenuto
Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricercaINIZIO_TESTO_DA_INDICIZZARE
PROGRAMMA DI RICERCA
italiano - english
Unità di Ricerca
Programmi di ricerca simili:
- 1 - Systems Biology: modellazione, linguaggi e analisi (Sybilla)
- 2 - Analisi di sistemi di Riduzione mediante sistemi di Transizione (ART)
- 3 - Modellizzazione Matematica del Comportamento Naturale e Artificiale
- 4 - Modellazione dinamica e controllo di strutture meccaniche complesse caratterizzate da parametri incerti
- 5 - Metodologie avanzate per il controllo di sistemi ibridi
- 6 - Sintesi automatica di modelli astratti a partire da dati temporali o spaziali
- 7 - Sistemi ad oggetti estendibili (EOS)
- 8 - Comprensione ab-initio delle proprieta' strutturali, elettroniche, ottiche di sistemi di semiconduttori nanostrutturati e a bassa dimensionalita'
- 9 - Analisi sperimentale, modellazione e simulazione di reattori slurry per l'abbattimento di inquinanti
- 10 - Future applicazioni del paradigma peer-to-peer
Classificazione scientifico-disciplinare
- Area scientifico disciplinare: Scienze matematiche e informatiche
Classificazione brevettuale
- CHEMISTRY; METALLURGY
- BIOCHEMISTRY; BEER; SPIRITS; WINE; VINEGAR; MICROBIOLOGY; ENZYMOLOGY; MUTATION OR GENETIC ENGINEERING
- MICRO-ORGANISMS OR ENZYMES; COMPOSITIONS THEREOF (biocides, pest repellants or attractants, or plant growth regulators, containing micro-organisms, viruses, microbial fungi, enzymes, fermentates or substances produced by or extracted from micro-organisms or animal material A01N63/00; food compositions A21, A23; medicinal preparations A61K; chemical aspects of, or use of materials for, bandages, dressings, absorbent pads or surgical articles A61L; fertilisers C05); PROPAGATING, PRESERVING OR MAINTAINING MICRO-ORGANISMS (preservation of living parts of humans or animals A01N1/02); MUTATION OR GENETIC ENGINEERING; CULTURE MEDIA (micro-biological testing media C12Q)
- BIOCHEMISTRY; BEER; SPIRITS; WINE; VINEGAR; MICROBIOLOGY; ENZYMOLOGY; MUTATION OR GENETIC ENGINEERING
- PHYSICS
- COMPUTING; CALCULATING; COUNTING (score computers for games A63; combinations of writing applicances with computing devices B43K29/08)
- COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS [N0004]
- EDUCATION; CRYPTOGRAPHY; DISPLAY; ADVERTISING; SEALS
- EDUCATIONAL OR DEMONSTRATION APPLIANCES; APPLIANCES FOR TEACHING, OR COMMUNICATING WITH, THE BLIND, DEAF OR MUTE; MODELS; PLANETARIA; GLOBES; MAPS; DIAGRAMS (devices for psychotechnics or for testing reaction times A61B5/16; games, sports, amusements A63; projectors, projector screens G03B)
- COMPUTING; CALCULATING; COUNTING (score computers for games A63; combinations of writing applicances with computing devices B43K29/08)
Classificazione geografica
- Regione: Toscana
Bibliografia
[ACH95] Alur, Courcoubetis, Halbwachs, Henzinger, Ho, Nicollin, Olivero, Sifakis, Yovine. The Algorithmic Analysis of Hybrid Systems. TCS 138 1995[ABI01] Alur, Belta, Ivancic, Kumar, Mintz, Pappas, Rubin, Schug. Hybrid modeling and simulation of biomolecular networks. HSCC01, LNCS 2034 2001
[ADI02] Alur, Dang, Ivancic. Reachability Analysis of Hybrid Systems via Predicate Abstraction. HSCC02, LNCS 2289 2002
[ADI03a] Alur, Dang, Ivancic. Counter-example Guided Predicate Abstraction of Hybrid Systems. TACAS, LNCS 2619 2003
[ADI03b] Alur, Dang, Ivancic. Progress on reachability analysis of hybrid systems using predicate abstraction. HSCC, LNCS 2623 2003
[AD94] Alur, Dill. A theory of timed automata. TCS 126 1994
[AGAT02] Amonlirdviman, Ghosh, Axelrod, Tomlin. A hybrid systems approach to modeling and analyzing planar cell polarity. Sys. Bio. 2002
[AMPPS03] Antoniotti, Mishra, Piazza, Policriti, Simeoni. Modelling cellular behavior with hybrid automata: Bisimulation and collapsing. CMSB, LNCS 2602 2003
[APUM02] Antoniotti, Policriti, Ugel, Mishra. XS-systems: eXtended S-Systems and Algebraic Differential Automata for Modeling Cellular Behavior. HiPC 2002
[Ard02] Ardelean. The relevance of biomembranes for P systems, Fund. Inf. 49 2002
[Ard03] Ardelean. Molecular Biology of Bacteria and its Relevance for P Systems. WMC-CdeA, LNCS 2597 2003
[BAM03] Besozzi, Ardelean, Mauri. The potential of P systems for modelling the activity of channels in E. Coli. M.C., LNCS 2003
[BFMZ03] Besozzi, Ferretti, Mauri, Zandron. P Systems with Deadlock. BioSystems 70 2003
[BMPZ03] Besozzi, Mauri, Paun, Zandron. Gemmating P systems: Collapsing Hierarchies. TCS 296 2003
[BCMMT05] Barbuti, Cataudella, Maggiolo, Milazzo, Troina. A Probabilistic Model for Molecular Systems. Fund. Inf. 67 2005
[BMMT06a] Barbuti, Maggiolo, Milazzo, Troina. A Calculus of Looping Sequences for Modelling Microbiological Systems. Fund. Inf. 72 2006
[BCDPPQ] Brodo, Curti, Degano, Prandi, Priami, Quaglia. Formal Executable Descriptions of Bio Systems. IEEE QEST 2005
[BG05] Busi, Gorrieri. On the Computational Power of Brane Calculi. TCSB, to appear
[Bus05] Busi. On the Computational Power of the Mate/Bud/Drip Brane Calculus: Interleaving vs. Maximal Parallelism. M.C., LNCS 3850 2006
[Car05] Cardelli. Brane Calculi. Interactions of Bio Membranes. CMSB, LNCS 3082 2005
[CG98] Cardelli, Gordon. Mobile ambients. FOSSACS98, LNCS 1998
[CP05] Cardelli, Pradalier. Where membranes meet complexes, BioConcur 2005
[CMPM05] Casagrande, Mysore, Piazza, Mishra. Independent dynamics hybrid automata systems biology. AB 2005
[CPM05] Casagrande, Piazza, Mishra. Semi-Algebraic Constant Reset Hybrid Automata. CDC-ECC, IEEE 2005
[CD03] Chiaverini, Danos. A core modeling language for the working molecular biologist. CMSB, LNCS 2602 2003
[CCDM04] Chiarugi, Curti, Degano, Marangoni, R. VICE: a Virtual Cell. CMSB, LNCS 3082 2004.
[CE82] Clarke, Emerson. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. Logic of Prog. 1982
[CES86] Clarke, Emerson, Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8 1986
[CC79] Cousot, Cousot. Systematic Design of Program Analysis Frameworks. POPL 1979
[CDPB03] Curti, Degano, Priami, Baldari. Causal pi-calculus for Biochemical Modelling. CMSB, LNCS 2602 2003
[CDPB04] Curti, Degano, Priami, Baldari. Modelling biochemical pathways through enhanced pi-calculus. TCS 325 2004
[DL03] Danos, Laneve. Core formal molecular biology. ESOP, LNCS 2618 2003
[DL04] Danos, Laneve. Formal Molecular Biology. TCS 325 2004
[DP04] Danos, Pradalier. Projective Brane Calculus. CMSB, LNCS 3082 2005
[FB96] Fontana, Buss. The barrier of objects: from dynamical system to bounded organizations. Addison-Wesley 1996
[FM03] Franco, Manca. A membrane system for the leucocyte selective recruitment. Memb. Comp. 2003
[FH05] Franzle, Herde. Efficient Proof Engines for Bounded Model Checking of Hybrid Systems. ENTCS 133 2005
[FJ02a] Frisco, Ji. Info-energy P systems. DNA 2002
[FJ02b] Frisco, Ji. Towards a hierarchy of info-energy P systems. WMC-CdeA02, LNCS 2597 2003
[Gil77] Gillespie. Exact stochastic simulation of coupled chemical reactions. J.Ch.Phys. 81 1997
[Gil01] Gillespie. Approximate accelerated stochastic simulation of chemically reacting systems. J.Ch.Phys. 115 2001
[GL05] Gori, Levi. A new occurrence counting analysis for BioAmbients. APLAS05, LNCS 3780 2005
[GPB05] Giorgetti, Pappas, Bemporad. Bounded model checking of hybrid dynamical systems. CDC-ECC, IEEE 2005
[GP05a] Girard, Pappas. Approximate bisimulations for nonlinear dynamical systems. CDC-ECC, IEEE 2005
[GP05b] Girard, Pappas. Approx. bisimulations for constrained linear systems. CDC-ECC, IEEE 2005
[GP06] Girard, Pappas. Approx. simulation relations for hybrid systems. ADHS 2006
[GT01] Ghosh, Tomlin. Lateral Inhibition through Delta-Notch Signaling: A Piecewise Affine Hybrid Model. HSCC, LNCS 2034 2001
[GT04] ] Ghosh, Tomlin. Symbolic Reachable Set Computation of Piecewise Affine Hybrid Automata and its Application to Bio Modelling: Delta-Notch Protein. Syst. Bio. 1 2004
[GT05] ] Ghosh, Tomlin. An Algorithm for Reachability Computations on Hybrid Automata Models of ProteSignaling Networks. CDC-ECC, IEEE 2005
[Hoa85] Hoare. Communicating Sequential Processes. Prentice-Hall 1985 <br />[HHGT01] Holcombe, Holcombe, Gheorghe, Talbot. A hybrid machine model of rice blast fungus Magnaporthe grisea. IPCAT 2001
[Kit02] Kitano. Foundations of System Biology. MIT Press 2002
[Kop96] Kopke. The Theory of Rectangular Hybrid Automata. PhD thesis, Cornell U 1996
[LPS00] Lafferriere, Pappas, Sastry. O-minimal hybrid systems. Math. Control Sig. Syst. 13 2000
[Mar03] Marcus. Bridging P Systems and Genomics: A Preliminary Approach. WMC-CdeA02, LNCS 2597 2003
[Mil89] Milner. Communication and Concurrency. Prentice-Hall 1989
[MPW92] Milner, Parrow, Walker. A calculus of mobile processes. I&C 100 1992
[Mis02] Mishra. A Symbolic Approach to Modeling Cellular Behavior. LNCS 2552 2002
[NOMK99] Nagasaki, Onami, Miyano, Kitano. Bio-calculus: Its concept and molecular interaction. Genome Infor. 10 1999
[Nak72] Nakanishi. Stochastic analysis of an oscillating chemical reaction. J.Phys. Soc. Jap. 32 1972
[Nis02] Nishida. Simulations of Photosynthesis by a K-Subset Transforming System with Membranes. Fund. Inf. 49 2002
[Pau02] Paun, Membrane Computing: An Introduction. Nat. Comp. Series 2002
[Pnu81] Pnueli. The temporal semantics of concurrent programs. TCS 13 1981
[PQ04] Priami, Quaglia. Beta binders for bio interactions. CMSB, LNCS 3082 2005.
[PQ05] Priami, Quaglia. Operational patterns in Beta-binders. TCSB 2005
[PRSS01] Priami, Regev, Silverman, Shapiro. Application of a stochastic passing-name calculus to representation and simulation of molecular processes. IPL 80 2001
[PV94] Puri, Varaiya. Decidability of hybrid systems with rectangular differential inclusions. CAV, LNCS 818 1994
[QS82] Queille, Sifakis. Specification and verification of concurrent systems. Int. Symp. Prog. 1982
[RPSCS04] Regev, Panina, Silverman, Cardelli, Shapiro. BioAmbients: An Abstraction for Bio Compartments. TCS 325 2004
[RSS01] Regev, Silverman, Shapiro. Representation and Simulation of Biochemical Processes Using the pi-Calculus Process Algebra. Pacific Symp. Biocomp., WSP 2001
[SFTT01] Suzuki, Fujiwara, Tanaka, Takabayashi. Artificial Life Applications of a Class of P Systems: Abstract Rewriting Systems on Multisets, Multiset Processing. LNCS 2235 2001
[SOT03] Suzuki, Ogishima, Tanaka. Modeling the p53 signaling network by using P systems. M.C. 2003
[STT00] Suzuki, Takabayashi, Tanaka. Adaptive Behavior a Tritrophic Interactions Consisting of Plants, Herbivors and Carnivores. SAB 2000
[ST00] Suzuki, Tanaka. Chemical Evolution Among Artificial
Proto-cells. Artif. Life 7 2000
[VPCD03] Vasilco, Popescu, Chiurtu, Dascalu. The Architecture for Living Structures-A Possible Basis for Molecular Computing. LNCS 2597 2003
Parole Chiave
BIOLOGIA DEI SISTEMI, BIOCONCORRENZA, CALCOLI E MODELLI ISPIRATI DALLA BIOLOGIASistemi e calcoli di ispirazione biologica e loro applicazioni -- BISCA
Università di PisaAbstract
Intendiamo sviluppare e usare metodi tipicamente informatici per descrivere, analizzare e realizzare in silico sistemi biologici. Oltre a tale modellizzazione, ci aspettiamo che i meccanismi con cui la materia vivente si organizza e interagisce ci suggeriranno nuovi paradigmi di computazione e nuovi formalismi utili nell’intera area delle scienze e tecnologie dell’informazione.Il progetto sarà focalizzato su linguaggi e modelli per la specifica di sistemi biologici, per la simulazione della loro dinamica e per la verifica formale di sue proprietà.
Ci concentreremo soprattutto sulla specifica e l’analisi delle interazioni intra- ed inter-cellulari. Le descrizioni di questi fenomeni includeranno sia aspetti qualitativi, tra cui relazioni causa-effetto, e aspetti quantitativi, per esempio quelli dipendenti dal tempo o da distribuzioni di probabilità la cui descrizione è cruciale per modellare sistemi biologici. Tali aspetti qualitativi e quantitativi richiedono nuove estensioni e arricchimenti alle tecniche automatiche di analisi di cui disponiamo e lo sviluppo di nuovi modi e tecniche.
Intendiamo usare meccanismi linguistici e modelli che siano specificamente ritagliati per descrivere e manipolare aspetti della materia vivente quali reazioni bio-chimiche, vie metaboliche e membrane. Sarà di conseguenza necessario adattare modelli e primitive linguistiche esistenti e svilupparne di nuovi.
Le nostre proposte saranno messe a punto, collaudate e convalidate su 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 strumenti software prototipali, basati sulle teorie che svilupperemo nella prima fase del lavoro.
Il successo del progetto confermerà il 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. <<<
Coordinatore Scientifico del Programma di Ricerca
Pierpaolo Degano Università degli Studi di PISAObiettivo del Programma di 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 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 strumenti software prototipali, basati sulle teorie che andremo sviluppando nella prima fase del lavoro.
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 celle 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. Infatti tali sistemi sono molto simili a quelli biologici. Entrambi sono composti da un gran numero di agenti di calcolo indipendenti, distribuiti, mobili, che scambiano informazioni e procedono autonomamente nel calcolo. I risultati del nostro progetto avranno quindi una ricaduta quasi immediata sull’importante campo dei servizi e delle applicazioni in rete. <<<
Durata
24 mesiBase di partenza scientifica nazionale o internazionale
I recenti e spesso sorprendenti sviluppi in biologia hanno prodotto una grande quantità di dati sulla struttura della materia vivente. Si consideri ad esempio il successo dello Human Genome Project. Molto minori sono invece le conoscenze sulle funzioni biologiche delle cellule e dei loro componenti. Perciò negli ultimi anni l’interesse scientifico si è spostato dalla struttura alla funzionalità, ed è nato un nuovo paradigma, detto biologia dei sistemi [Kit02], che muove dal classico approccio riduzionistico verso una comprensione dei meccanismi della vita a livello di sistema.C’è un generale accordo nella comunità scientifica che l’informatica sarà indispensabile alla biologia come la matematica lo è stata per la fisica. Ad esempio, la mappatura del genoma umano sarebbe stata impossibile senza calcolatori, algoritmi e sintassi per descriverne le strutture: è stato cruciale rappresentare il DNA come un linguaggio formale su un alfabeto di quattro caratteri e usare algoritmi di ricerca e confronto su stringhe. Allo stesso modo, l’informatica appare essenziale per capire il comportamento degli organismi viventi: passare da strutture a funzioni significa dotare la sintassi di una semantica.
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. Inoltre, la modellazione di tali sistemi non è solo un’area di applicazione importante per l’informatica, ma è anche un ambiente stimolante per il progetto e il collaudo di idee innovative della stessa disciplina. In effetti, la tecnologia dell’infomazione si presenta sempre più come abilitante per altre aree, a sua volta soggetta a stimoli di queste, specialmente dalle scienze della vita. In questo dominio il nostro approccio generale si propone di produrre tecniche e strumenti per descrivere e scoprire conoscenza in sistemi biologici complessi da un punto di vista strutturale e comportamentale.
Siamo perciò fautori di una convergenza tra informatica e scienze della vita, auspicando uno spostamento paradigmatico anche sul lato dell’informatica e un arricchimento reciproco delle due discipline. La letteratura scientifica ci sostiene: alle strette connessioni tra sistemi biologici e di calcolo, si aggiungono molte osservazioni che indicano che tecniche e strumenti dei linguaggi di programmazione possono esser usati per modellare, analizzare e simulare il comportamento dinamico di sistemi biologici. Infatti questi 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 spesso presentati come macchine astratte, il cui comportamento è specificato da transizioni che cambiano lo stato interno della macchina astratta. Un’altra somiglianza è che entrambi i tipi di sistemi risultano dalla combinazione di parti più piccole. Di solito, il comportamento delle componenti è ben conosciuto, ma quello della loro composizione resta largamente inaspettato, esibendo proprietà emergenti. Il vantaggio dei sistemi di calcolo è che le loro macchine astratte sono facilmente realizzate, i sistemi corrispondenti eseguiti e il loro comportamento esaminato. Le proprietà emergenti sono mostrate esplicitamente e rese disponibili per l’analisi e,se non volute, il progettista del sistema di calcolo può modificare la macchina astratta associata fino ad ottenere il comportamento richiesto.
Di seguito affrontiamo in maggior dettaglio tre approcci complementari alla specifica delle macchine astratte, saottolineandone le connessioni con la biologia di sistemi. Questi approcci sono centrali alle aree di ricerca dell’informatica dedicate a modelli computazionali, linguaggi e strumenti di programmazione. Intuitivamente, l’approccio linguistico offre un modo preciso, basato sulla logica formale, per descrivere i passi di calcolo elementari; da questi, si ottengono le transizioni della macchina astratta in modo puramente composizionale. Un punto di vista differente considera direttamente la macchina astratta come un automa e si concentra su metodi e strumenti efficienti per validare il comportamento del sistema. Il terzo classico modo è duale al precendente: la macchina astratta è rappresentata come una grammatica, o più generalmente come un sistema di riscrittura, ereditando dalla teoria nota un vasto repertorio di risultati e tecniche di prova.
Gli iniziatori dall’approccio linguistico sono Fontana e Buss [FB96] che usano il lambda-calcolo per modellare sistemi biochimici. Il lavoro pionieristico di Regev, Silvermann e Shapiro [RSS01] evidenzia le somiglianze tra i sistemi di calcolo distributi concorrenti e mobili e i sistemi biologici, tra cui reti metaboliche, regolatrici di geni, e di segnali. I sistemi biologici consistono di milioni di componenti attivi simulatanemente, che interagiscono per raggiungere obbiettivi, per cosí dire comuni. Tali interazioni sono principalmente binarie e avvengono solo se i componenti coinvolti sono collocate opportunamente, p.e. sono abbastanza vicine, non sono divise da una membrana, l’affinità o la propensione di interazione è sufficientementa alta. Infine le interazioni influenzano il comportamento futuro dell’intero sistema seppure esse avvengano in loco. Tutte queste caratteristiche descrivono altrettanto bene i sistemi distribuiti concorrenti e mobili, tranne forse che per il fatto che i sistemi artificiali hanno un numero minore di componenti. Ci sono vari calcoli di processo che specificano forma e comportamento dei sistemi e che ne consentono l’analisi. Alcuni di loro sono già stati usati ed estesi per applicarli alla biologia. Particolarmente rilevante è la proposta di Priami et al. che in [PRSS01] arricchiscono il pi-calcolo con aspetti quantitativi, sfruttando una precedente variante stocastica di Priami. Curti, Degano, Priami e Baldari usano l’Enhanced pi-calcolo per rappresentare aspetti del comportamento dei processi relativi a causalità e località in [CDPB04] e in [CCDM04] per specificare e analizzare un’ipotetica cellula con un genoma il piú ridotto possibile. Questo procariota virtuale esibisce in silico un comportamento simile a quello dei procarioti reali, e quindi risulta essere un buon modello. Tra i calcoli usati in biologia dei sistemi menzioniamo anche il bio-calculus proposto da Nagasaki et al. in [NOMK99], un ambiente che include un’editore di equazioni, un interprete e un’interfaccia grafica, cosicché le vie metaboliche sono descritte usando equazioni biochimiche convenzionali. Recentemente Regev et al. hanno proposto BioAmbients [RPSCS04], una variante di Ambients [CG98] in cui i compartimenti sono specificati come una gerarchia di ambienti di confine, che può essere modificata con operazioni che hanno un’immediata interpretazione biologica, p.e. le comunicazioni padre-figlio rappresentano bene l’interazione tra composti che si trovano nel citosol e nel nucleo. I Brane Calculi di Cardelli [Car05] sono una famiglia di calcoli per descrivere le interazioni di membrane annidate dinamicamente. La differenza principale rispetto agli approcci precedenti è che le entità attive risiedono sulle e non dentro le membrane. Le sue primitive di interazione sono classificate in due gruppi: endocitosi/esocitosi e fusione/fissione. L’espressività di questi gruppi è studiata in [BG05,Bus05]. Il Projective Brane Calculus [DP04] è un raffinamento di Brane Calculi dove le azioni sulla membrane sono orientate e ripartite in due insiemi, a seconda che operino sullo strato esterno o interno della membrana. In Beta-binders [PQ04,PQ05], processi à la pi-calcolo sono incapsulati in scatole che interagiscono l’un l’altra mediante siti di interazione tipizzati. Le primitive permettono di aggiungere, nascondere e rivelare un sito; due ulteriori operazioni, split e join ,cambiano la struttura delle scatole. Recentemente Beta-binders è stato esteso a trattare aspetti stocastici [DPPQ06] per consentire il modello quantitativo di fenomeni biologici. Danos e Laneve [DL03,DL04] e Chiaverini e Danos [CD03] hanno proposto Core Formal Molecular Biology a partire dalle primitive di base del pi-calcolo. Il comportamento dei processi (composti) e di insiemi di processi (soluzioni) è dato da regole di riscrittura che modellano le attività di attivazione, sintesi e complessazione. Recentemente Cardelli e Pradalier [CP05] hanno proposto un calcolo che combina operazioni di complessazione/decomplessazione su molecole con operazioni di interazione di membrane, nello stile del Projective Brane Calculus. Strettamente collegato all’approccio sommariamente descritto è il rilevante lavoro fatto per rappresentare sistemi biologici mediante reti di Petri o modelli correlati; ne omettiamo una rassegna, a causa di mancanza di spazio.
Come menzionato, c’è una grande varietà di strumenti, basati sulla semantica, per l’analisi del comportamento di processi concorrenti, tipicamente per far ricerche nello spazio degli stati o per verificare varie equivalenze e preordini. Tra questi, ricordiamo il concurrency workbench (www.dcs.ad.ac.uk/home/cwb) e il mobility workbench (www.it.uu.se/research/group/mobility/mwb), e alcuni strumenti che trattano esplicitamente gli aspetti stocastici, come il workbench PEPA (www.dcs.ed.ac.uk/pepa/) e TwoTowers (www.uniurb.it/bernardo/twotowers/); vi sono infine simulatori che usano l’algoritmo di Gillespie [Gil77] negli interpreti del pi-calcolo stocastico, quali BioSpi (www.wisdom.weizmann.ac.il/~biopsi/) e SPiM (www.doc.ic.ac.uk/~anp/spim/). A causa della complessità intrinseca dei sistemi biologici appaiono anche particolarmente interessanti tecniche di analisi statica (p.e. l’interpretazione astratta [CC79]) per inferire in modo efficiente informazione approssimata sul loro comportamento. Infatti simulatori o verificatori automatici hanno a volte una complessità inaccettabile e prestazioni ridotte. In [GL05] è stato proposta una nuova interpretazione astratta di Bio-ambients capace di affrontare aspetti sia quantitativi che causali dei sistemi biologici.
Nell’approccio basato su sistemi di riscrittura, un sistema biologico è rappresentato da un termine e il suo comportamento è definito da regole di riscrittura. Quest’approccio è stato usato per modellare reazioni biochimiche in [Gil77,Gil01,Nak72,BCMMT05]. Una singola reazione è rappresentata da una regola di riscrittura e la scelta di quale regola applicare tra le regole applicabili è guidata da una probabilità associata con la regola, che ne rappresenta la velocità. Quest’approccio può essere combinato con quello linguistico. Ad esempio, in [BMMT06a] è stato definito un nuovo calcolo, chiamato Calculus of Looping Sequences, i cui termini descrivono lo stato del sistema biologico e sono costruiti a partire da elementi di base. In generale, il comportamento di un sistema è descritto da un insieme di regole di riscrittura da applicare ai termini, che possono essere riarrangiati usando congruenze strutturali. Tali regole di riscrittura sono facilmente implementabili, e portano quindi allo sviluppo di simulatori. Paun [Pau02] ha introdotto un nuovo modello computazionale basato sull’idea che tutti i processi a livello cellulare, dove reazioni chimiche e flusso di materiali ha luogo tra compartimenti differenti, possano essere visti come processi di calcolo. Un sistema biologico non banale è un costrutto in cui vari componenti eseguono le proprie computazioni, che si scambiano i propri risultati. Membrane di vario tipo tengono i componenti ben delimitati , li separano e agiscono come barriere semipermeabili assicurando che certe sostanze stiano sempre entro il compartimento, mentre altre ne stiano fuori. A ciascuna membrana sono associati oggetti (filamenti di DNA, molecole, ecc…) e regole dinamiche (reazioni chimiche). Le regole operano sugli oggetti modificandoli e sulla struttura delle membrane dissolvendole o dividendole e creandone di nuove. Le molecole presenti nella cellula si possono muovere da una regione all’altra oltrepassando le membrane. Questi sistemi sono stati usati per modellare aspetti energetici connessi alle reazioni cellulari [FJ02a,FJ02b]; sono stati considerati simulazione di fotosintesi [Nis02], processi di comunicazione dentro la cellula [BAM03,BMPZ03,SOT03], e altri aspetti di organismi e sistemi biologici [Ard02,Ard03,BFMZ03,FM03,HHGT01,Mar03,SFTT01,STT00,ST00,VPCD03].
Molti sistemi biologici hanno un comportamento misto discreto/continuo difficilmente caratterizzabile con modelli discreti o continui. Il loro comportamento è regolato da una legge dinamica continua che tien conto di concentrazioni di sostanze e gradienti; inoltre tale legge cambia in dipendenza dallo stato del sistema. Per modellare questo tipo di sistemi, chiamati ibridi, Alur et al. hanno introdotto in [ACH95] gli automi ibridi che intuitivamente sono automi a stati finiti, con variabili continue che cambiano secondo un insieme di leggi continue e che caratterizzano ciascun nodo discreto dell’automa stesso. L’uso di automi ibridi per modellare reti bio-molecolari è descritto da Alur et al. [ABI01] e da Mishra [Mis02]. Amonlirdviman et al. [AGAT02] ne dimostra l’utilità modellando la polarità della cellula planare Drosophila. Partendo dalla formulazione di S-System di Savageau e Voit, Antoniotti et al. [AMPPS03] usano un automa per ampliare l’insieme dei sistemi rappresentabili, usando in seguito Full-fledged Hybrid Automata [APUM02]. Ghosh and Tomlin preseno modelli di delta-notch [GT01,GT04] e di una rete di segnali di una proteina [GT05]. Casagrande et al. [CMPM05] suggeriscono un semplice modello di automa ibrido per la chemiotassi di E.coli. Una volta specificato formalmente il sistema biochimico occorre verificarne le proprietà su tale descrizione. Logiche temporali [Pnu81] e model checking [CE82,QS82,CES86] sono largamente usati sia per esprimere che per provare proprietà di sistemi ibridi. Le prime estendono la logica proposizionale ed esprimono proprietà di sequenze di transizioni; oltre ad usare proposizioni atomiche e connettivi booleani tradizionali, le logiche temporali possono specificare proprietà come “prima o poi varrà la proprietà P”, “d’ora in poi la proprietà Q vale” o “la proprietà R non varrà mai”. Il model checking è una tecnica automatica per verificare proprietà su un modello con molti vantaggi rispetto ad approcci basati su simulazione o testing: esso garantisce la verifica corretta e completa di una proprietà che tratta il comportamento complessivo, mentre simulazione e testing considerano solo alcuni dei possibili percorsi. In generale il problema del model checking per i sistemi ibridi è indecidible [ACH95], ma ci sono due modi per aggirare questo problema. Il primo è ritagliare classi per cui il problema è decidibile [ACH95,AD94,PV94,Kop96,LPS00,CMPM05, CPM05]. Tuttavia ciò richiede vincoli assai restrittivi, che ne rendono difficile l’uso nell’analisi dei sistemi reali. Il secondo modo impiega analisi approssimate per ottenere risultati parziali, p.e. che una proprietà vale per almeno 10’ dalle condizioni iniziali; tra queste analisi vi sono il model checking limitato [GPB05,FH05], l’interpretazione astratta [ADI02,ADI03a,ADI03b], e la riduzione per quoziente [GP05a,GP05b,GP06]. <<<



