RICERCA ITALIANA     

Programma di ricerca

Sistemi e calcoli di ispirazione biologica e loro applicazioni -- BISCA

Università di riferimento

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

Responsabile dell'Unità di ricerca

Alberto Policriti

Descrizione

Nell'ambito del presente progetto di ricerca, l'unità di Udine lavorerà sui quattro seguenti argomenti:

• una teoria composizionale degli automi ibridi;
• un approccio algebrico al model checking di sistemi biologici;
• Ariane: un meta-tool per il model checking degli automi ibridi;
• un approccio misto algebre dei processi – automi.


Teoria composizionale degli automi ibridi

Usualmente i sistemi reali sono costituiti da molte componenti che interagiscono tra di loro. Sfortunatamente, i modelli che descrivono questi sistemi possono avere un numero di stati discreti esponenziale rispetto al numero di componenti del sistema. Questo problema è noto con il nome di problema dell'esplosione degli stati. Per risolvere questo problema, sono state proposte differenti tecniche: le più note sono il model checking simbolico, il model checking astratto, le riduzioni per ordini parziali e le riduzioni per equivalenza. Tutte queste tecniche usano un approccio dall'alto verso il basso, partendo dal sistema completo cercano di ridurre lo spazio degli stati. Questo approccio ha due problemi principali: prima di tutto assume di lavorare su tutta la rappresentazione del sistema e questa è un'assunzione forte per molti sistemi biologici che hanno centinaia di componenti. In secondo luogo, questa metodologia non sfrutta la possibilità di verificare le parti decidibili del sistema. Per queste ragioni, è auspicabile l'utilizzo di un approccio dal basso verso l'alto in cui ogni componente del sistema sia verificata separatamente ed i risultati siano combinati in modo da dedurre il comportamento globale del sistema. Il nostro obbiettivo sarà quello di individuare le proprietà degli automi che sono necessarie a raggiungere questo scopo.

Approccio algebrico al model checking di sistemi biologici

Negli ultimi anni, ha cominciato ad essere diffusamente studiato l'approccio di sfruttare i risultati di Tarski e l'eliminazione dei quantificatori per studiare gli automi ibridi. Per esempio, Jirstrand [38] ha mostrato l'utilizzo di Qepcad per i problemi raggiungilibità, insiemi stazionarizzabili, intervalli di output controllabili e studio delle curve nel contesto del progetto di sistemi di controllo non lineari. In seguito, Anai [39] e Franzle [40] hanno suggerito indipendentemente l'uso dell'eliminazione dei quantificatori per la verifica degli automi ibridi polinomiali. Franzle ha provato che la verifica di proprietà di sicurezza, la ricorrenza di stati e la raggiungibilità sono semi-decidibili tramite l'eliminazione dei quantificatori [41] e ha sviluppato un “motore di verifica” per il bounded model checking [42]. Più recentemente, Lafferiere e al. [43] hanno descritto un metodo basato sull'eliminazione dei quantificatori per la verifica simbolica della raggiungibilità su campi vettoriali lineari. In seguito, Ratschan e She [44] hanno suggerito un nuovo tipo di raffinamento basato sulla propagazione dei vincoli per la verifica delle proprietà di sicurezza un sistema ibrido con equazioni differenziali autonome. Altri recenti sviluppi includono il lavoro integrazione del bounded model checking e della verifica induttiva di Becker e al. [45]. Lanotte e Tini [46] hanno recentemente provato che, dato un qualsiasi sistema ibrido, l'automa semi-algebrico ottenuto approssimando ciascuna formula con il corrispondente polinomio di Taylor è una sovra approssimazione del sistema di partenza. Casagrande e al. hanno sfruttato i risultati di Tarski per fornire un semplice modello ibrido per la chemotaxis dell'E. coli [10] e provare la decidibilità del problema del model checking su una classe di automi ibridi, chiamata SACoRE, le cui dinamiche sono inclusioni. Intendiamo investigare il dominio biologico tramite l'approccio algebrico cercando di individuare sia specifiche classi decidibili di automi ibridi che tecniche di model checking approssimato basate sui vincoli fisici dei sistemi e la cylindrical algebraic decomposition parziale.

Ariande: a meta-tool for hybrid automaton model checking

Per permettere lo studio di quegli automi ibridi per cui il problema della raggiungibilità è indecidibile, sono stati sviluppati molti programmi software basati su tecniche di approssimazione [47, 48, 49, 50, 51, 52]. I più importanti tra questi sono HyTech [29], d/dt [30], Checkmate [31], UPPAAL [32], and KRONOS [33]. Questi strumenti hanno molte proprietà interessanti quali la possibilità di fare model checking o interfaccie grafiche per la definizione degli automi. Tuttavia, essi hanno due svantaggi. Primo, questi software hanno licenze restrittive e per alcuni non è nemmeno disponibile il codice sorgente. Senza l'accesso al codice o la possibilità di modificarlo, gli utenti non possono ne' ottimizzare i software per specifiche classi di problemi ne' controllare che gli algoritmi siano implementati corretamente, Secondo, questi software non supportano la valutazione dell'insieme di raggiungibilità con precisione infinita. Infatti, come provato da Collin e Lygeros in [53], nonostante l'uso di strutture dati con precisione infinita, l'approssimazione con precisione arbitraria dell'insieme di raggiungibilità non è in generale computabile.
Per superare queste limitazioni, proponiamo un ambiente per la verifica dei sistemi ibridi che ha tre obbiettivi principali. Il primo obbiettivo è quello di realizzare un ambiente di sviluppo in cui poter definire tecniche di rappresentazione dello spazio e algoritmi per l'analisi di raggiungibilità. Il secondo obbiettivo è quello di definire un software che integri e implementi gli algoritmi e le tecniche di rappresentazione esistenti consentendo all'utente di scegliere il metodo migliore per le sue esigenze. L'ultimo obbiettivo è di supportare la rappresentazione approssimata in precisione arbitraria dell'evoluzione di un automa ibrido.
Questo meta-tool, chiamatao Ariane, offrirà uno schema ad alto livello basato su moduli generali progettato in modo tale da consentire una più facile personalizzazione per le varie esigenze. Il pacchetto software sarà rilasciato nella formula open source (codice aperto) in modo che differenti gruppi di ricerca possano contribuire al progetto sviluppando nuove strutture dati, algoritmi e euristiche. Ariane implementerà i principali metodi geometrici per la rappresentazione dello spazio basati su simplex, parallelotopi, zonotopi e poliedri parametrizzandoli rispetto al dominio dei reali. Inoltre, consetirà all'utente di definire funzioni multivariate dell'insieme degli oggeti rappresentabili a se stesso e fornirà metodi di valutazione per tali funzioni.

Approccio misto algebre dei processi – automi

Come ultimo campo di interazione tra formalismi capaci di modellare situazioni biologicamente significative, menzionamo la potenziale connessione tra formalismi basati su algebre di processo ed automi ibrdi.
Abbiamo in programma di studiare la corrispondenza tra formalismi basati su algebre di processo e automi (ibridi) quale strumento per chiarificare la espressivita' relativa tra una una descrizione interna (basata sulla comunicazione) ed una esterna (basata su quantita' osservabili principalmente mediante sistemi di equazioni differenziali) dello stesso sistema biologico.
Una tale corrispondenza dovrebbe essere stabilita attraverso la messa a punto di specifici risultati di transfer che permettano, per esempio, di passare da una rappresentazione mediante il pi-calcolo stocastico (si veda [54,55,56,57]) e una rappresentazione basata su S-sistemi (si veda [59]).
Nonostante la semplicita' sintattica del pi-calcolo, il linguaggio e' altamente espressivo e produce una dimostrazione pratica di come, mediante un insieme estremamente limitato di primitive e di strumentazione sintattica, possano essere rappresentati scenari di cominicazione veramente complessi.
Una proprieta' particolarmente interessante (e potente) del pi-calcolo, e' la possibilita' di comunicare nomi di canali sui canali stessi, proprieta' che conferisce all'utente l'possibilita' di ridisegnare la rete di comunicazione ad execution time.
Un ingrediente quantitativo non puo' mancare se si hanno in mente applicazioni biochimiche e la soluzione naturale e' stata quella di introdurre quantita', da interpretarsi come rates di comunicazione, da associare ad ogni canale. Tali rates sono usate nella macchina astratta che implementa il pi-calcolo per definire la "competizione stocastica" che governa l'esecuzione e stabilisce la base per la simulazione al computer di (famiglie di) interazioni biochimiche regolate da parametri quantitativi. La questione dell'implementazione del pi-calcolo stocastico e' stata risolta con l'uso di un algoritmo (l'algoritmo di Gillespie) che era stato originariamente sviluppato per la simulazione numerica dell'evoluzione temporale di sistemi molecolari in fase gassosa.
Gli S-sitemi hanno il merito di fornire una sorta di "forma normale"--un macchinario matematico naturale ed uniforme--per la modellazione biochimica, e questa e' la principale ragione per il loro uso nel nostro approccio. La definizione di S-sistema impone condizioni che dovono essere soddisfatte dal sistema stesso per garantire l'obbedienza delle leggi di conservazione di massa, delle relazioni stoichiometriche, ecc. Un S-sistema e' una quadrupla S = (DV, IV ,DE,C) dove:
• DV = {X1, . . . ,Xn} e' un insieme finito e non vuoto di variabili dipendenti varianti sui loro rispettivi domini D1, . . . ,Dn ;
• IV = {Xn+1, . . . ,Xn+m} e' un insieme finito di variabili indipendenti varianti sui loro rispettivi domini Dn+1, . . . ,Dn+m ;
• DE e' un insieme di equazioni differenziali non-lineari in uno specifico formato che governano la dinamica di ogni variabile dipendente in termini di altre variabili dipendenti e di variabili indipendenti.
Il comportamento di un S-sistema puo' essere simulato computando i valori approssimati delle sue variabili ad istanti di tempo successivi e dipende strettamente dalla scelta dei parametri coinvoldi nelle equazioni differenziale al centro della rappresentazione.
Il punto chiave nello specifico del nostro piano e' quello di avere una corrispondenza (automatica) tra i due precendenti formalismi che renda le loro specifiche capacita' e le specifiche possibilita' espressive in senso quantitativo dei due insiemi di parametri coinvolti.
Consideriamo questo passo come un prerequisito necessario per stabilire un legame piu' 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. Un tale passo sarebbe poi seguito dalla determinazione della parte discreta dell'automa, cioe' della parte caratterizzante il "controllo discreto" del sistema biologico sulla sua dinamica.