Formal Methods Laboratory

Principalul scop al conferintei “2nd International Meeting on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2008)” care a avut loc in perioada 3-4 Septembrie 2008 la Iasi a fost de a aduce la un loc cercetatori ce lucreaza in sistemele membranare si in algebrele de procese inspirate din biologie (ambienti, calcul membranar – brane calculus, etc.) pentru a prezenta cercetari recente si pentru a discuta noi idei legate de aceste formalisme, proprietatile lor si relatiile dintre ele.
Anul acesta marcheaza aniversarea a 10 ani de la introducerea sistemelor membranare, ocazie cu care unul dintre invitati a fost creatorul acestui formalism, anume domnul Gheorghe Paun, care a prezentat structura viitoarei sale carti care cuprinde o sinteza a tot ce a fost realizat in acest domeniu.
Comitetul de program a fost unul cu mare vizibilitate internationala:

Lucrarile prezentate la aceasta conferinta au fost publicate la Editura Universitatii “Alexandru Ioan Cuza” [L11], iar unele lucrari vor fi selectate si extinse pentru a fi publicate intr-un volum special al seriei Electronic Notes in Theoretical Computer Science.

In lucrarea [L4] am introdus calculul stochastic de fuziune, o extindere a calculului de fuziune, pentru a modela si studia sisteme biologice complexe, in particular procesul de regularizare a genelor. In sistemele complexe interactiunile au loc la scara larga, lucru dificil de modelat utilizand algebrele de procese, deoarece acestea lucreaza cu interactiuni intre doi agenti. Aceasta dificultate este surmontata de catre calculul stochastic de fuziune, ce foloseste clase de echivalenta pentru nume in cazul interactiunilor multiple, avand o semantica data de un sistem tranzitional stochastic etichetat. Utilizand acest calcul, am modelat regularizarea unei gene in bacterii. Urmand directia data de Regev si Shapiro[6], am reprezentat membrii populatiei biomoleculare drept procese si evenimentele drept comunicari. Am folosit fuziuni ale numelor proceselor pentru a reprezenta interactiunile intre mai multe procese. Fuziunile sunt echivalente de nume, facand posibila inlocuirea intr-un termen a numelor echivalente. In ceea ce priveste latura stochastica, am utilizat cu precadere distributia exponentiala. Mai precis, etichetele sistemului tranzitional folosit sunt perechi formate dintr-o actiune si rata distributiei. Pentru procese ce ruleaza in paralel, definim distributia obtinuta in cazul sincronizarii lor. De asemenea, am extins notiunea de hiperbisimulare la calculul stochastic de fuziune, am demonstrat ca hiperechivalenta astfel obtinuta este o congruenta si am prezentat un sistem axiomatic pentru hiperbisimularea stochastica.

Lucrarea [L5] continua tema analizei sistemelor biologice complexe cu un numar mare de interactiuni intre procese. Pentru a surprinde relatia intre evolutia spatială si cea temporala a proceselor am introdus in [L5] un nou formalism numit „TiMo” (Timed Mobility). In „TiMo” procesele migreaza intre locatii, primesc si transmit date, iar aceste actiuni pot fi controlate prin mecanisme de masurat timpul, numite „timers”. Printr-un „timer” poate fi specificat, de exemplu, un moment limita pana in care un proces trebuie sa primeasca sau sa transmita date; in cazul in care aceasta comunicare nu are loc pina la expirarea „timer”-ului, se incepe executia unui proces de siguranta. O caracteristica importanta a acestui formalism este data de faptul ca procesele isi pot comunica viitoare destinatii, i.e., nume de locatii in care trebuie sa se deplaseze. Interactiunea proceselor are loc doar cand acestea se afla in aceeasi locatie. In semantica operationala a acestui formalism, timpul este considerat discret, iar actiunile primitive (comunicare, deplasare) se efectueaza in mod maximal concurent. Modelul temporal al „TiMo” este asemanator cu cel considerat pentru retele Petri compozitionale cu timp. Din acest motiv, in [L5] este realizata si o translatare a formalismului nostru intr-un anumit tip de retele Petri. Aceasta translatare face ca „TiMo” sa beneficieze de posibilitatile de exprimare a paralelismului si cauzalitatii din retele Petri. Mai mult, astfel se pot utiliza tehnici de verificare deja concepute pentru proprietatile sistemelor modelate cu ajutorul „TiMo”.

In lucrarea [L1] am tratat problema inversarii procesului de calcul efectuat in cadrul unui sistem membranar. Aceasta problema este strans legata de gasirea legaturilor cauzale intre obiectele sistemului, ca si de notiunea de calcul reversibil [3]. Am tratat cazul sistemelor membranare cu reguli simple, ce produc obiecte cu o aceeasi destinatie. Cand sistemul in discutie are o singura membrana, inversarea regulilor sistemului este suficienta pentru a gasi configuratiile predecesoare, cu conditia ca multisetul de reguli aplicat sa fie revers valid. Aceasta conditie este foarte apropiata de cea de maxima validitate, demonstrand ca inversarea unui proces de calcul nu necesita un efort computational deosebit. In cazul sistemelor cu mai multe membrane este necesara si mutarea anumitor reguli intre membrane. Am sugerat si o solutie pentru sisteme in care regulile ce pot fi aplicate sunt de tip general.

MicroRNA-urile au fost decoperite in ultima decada si alaturi de alte categorii de RNA non-codant constituie o clasa de secvente genetice care suscita astazi un interes major din partea cercetătorilor din biologia moleculara, genetica si medicina, datorita fenomenului de interfenta mediata RNA (pe scurt, interferenta RNA) pe care il genereaza. Lucrarea [L6] prezinta yasMiR, o masina cu vectori-suport (SVM) conceputa pentru identificarea de microRNA-uri. Aceasta masina introduce doua caracteristici noi in raport cu celelalte SVM-uri care au fost create in acest domeniu:

SVM-ul creat de noi (yasMiR) a fost testat prin comparare directa cu Triplet-SVM, miPred si miR-abela. In toate cazurile, yasMiR a obtinut rezultate comparabile cu cele mai bune dintre rezultatele furnizate de miPred (cel mai performant dintre sistemele citate). In multe situatii, rezultatele noastre au fost chiar mai bune decit cele ale sistemului miPred. In plus, am testat daca inlocuirea clasificatorului SVM cu un alt clasificator, Random Forest (RF) conduce la rezultate mai bune decit cele obtinute de SVM pe datele noastre. Concluzia noastra este ca în general RF furnizeaza rezultate la acelasi nivel cu SVM, dar pe anumite seturi de date (de exemplu, pentru RNA-uri mesager), RF conduce la erori mai de clasificare.

Lucrarea [L7] este o versiune revizuita si extinsa a lucrarii prezentate la WRLA 2008. A fost reorganizata teoria care descrie semantica sistemelor membranare cu ajutorul controlorilor de strategii, au fost incluse implementari interleaving pentru comunicare si dizolvare. A fost finalizata implementarea in Maude, accesibila pe Web la adresa http://thor.info.uaic.ro/~rewps/. Aceasta implementare permite utilizarea LTL-model checkerului din Maude pentru verificarea de proprietati temporale ale sistemelor membranare.

Lucrarea [L8] este o versiune revizuita si extinsa a articolului cu acelasi nume prezentat la conferinta Prague International Workshop on Membrane Computing, p. 23-34, 2008. S-a definit notiunea de sistem de tranzitie distribuit abstract cu ajutorul caruia s-a descris forma logica modala de tip Hennessy-Milner atat pentru sistemele membranare cat si pentru teoriile din logica rescrierii. Am reusit sa dam o demonstratie formala a rezultatului privind exprimarea concurentei maximale a regulilor de evolutie in logica rescrierii si am adaugat un rezultat privind concurenta maximala a comunicarii si dizolvarii.

Lucrarea [L9] este o varianta extinsa si imbunatatita a lucrarii “Multisets and Their Encodings”, [2] prezentata la “Prague International Workshop on Membrane Computing” si raportata in cadrul etapei precedente. In urma prezentarii, am fost invitati sa trimitem o versiune extinsa care sa fie reevaluata si eventual publicata in IJFCS (revistă ISI, avand factor de impact). Multiseturile constituie principalul “ingredient” utilizat de membrane in cadrul proceselor de calcul.
            Fata de lucrarea menţionata, care a fost prezentata in rezumat in raportul fazei a V-a, a fost introdusa si studiata functia care asociaza oricarui multiset patratul normei sale. S-a demonstrat surjectivitatea acestei functii si s-a evaluat abaterea de la injectivitate, cu alte cuvinte s-a determinat, tot cu ajutorul teoriei numerelor, cate multiseturi au aceeasi norma.
            In [2] am obtinut un rezultant important care se refera la universalitatea, in sens Lagrange, patratului funcţiei norma pentru multiseturi peste un alfabet cu 4 litere (similar alfabetului ADN) si, chiar mai mult, minimalitatea numarului 4 in ceea ce priveste acest tip de universalitate. Acest rezultat au fost alaturate unor rezultate similare privind numărul 4 (cum ar fi [4] sau [7]), ca posibile explicatii matematice ale faptului ca alfabetul ADN are 4 litere.

O alta lucrare ce trateaza probleme legate de multiseturi este [L3]. Plecand de la teoria codificarii sursei, in aceasta lucrare am considerat ca sursa de informatie genereaza o secventa de multiseturi in loc de secventa de stringuri. Au fost introduse notiuni noi, similare celor pe stringuri, precum coduri fara submultiseturi, numite si multicoduri instantanee. A fost definita de asemenea lungimea medie pentru o codificare pe multiset. A fost prezentata o teorema in care se prezinta structura codurilor fara submultiseturi optimale pentru o sursa descrisa printr-o variabila aleatoare uniformă si a fost descris un algoritm pentru generarea acestor coduri optimale. Aceste rezultate sunt relevante mai ales in contextul in care pe canalul de comunicare nu este importanta ordinea transmiterii datelor, de exemplu in biologie trecerea unui transfer de sange printr-o vena poate fi vazuta ca un transfer de informatie intre un emitator si un receptor. In astfel de sisteme analiza teoriei codificarii unei surse de informatie utilizand multiseturi in locul stringurilor poate duce la rezultate cu un mare impact. In raportul tehnic [L10] se regaseste o prima incercare a abordarii teoriei compresiilor de date utilizand multiseturi. Sunt definite notiuni similare cu prefix-free codes, codificare, si lungimea medie a codificarii utilizand multiseturi in loc de stringuri. Se trateaza structura codurilor dintr-o codificare ce foloseste multiseturi pentru bazele 2 si 3.

[L1] O. Agrigoroaiei, G. Ciobanu. Dual P systems. Proceedings of WMC 2008
(Workshop on Membrane Computing), 45-59, 2008.

[L2] B. Aman, G. Ciobanu. Membrane Systems with Surface Objects. Proceedings of the International Workshop on Computing with Biomolecules (CBM 2008),17-29,2008.

[L3]C. Bonchiş, G. Ciobanu, G. Ghergu, C. Izbaşa, Data compression on multisets. Submultiset-free codes, Synasc08: 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. Timişoara, Romania, IEEE Computer Society, 2008

[L4] G. Ciobanu . From Gene Regulation to Stochastic Fusion, Lecture Notes in Computer Science, vol.5204, 51-63, 2008

[L5] G. Ciobanu, M. Koutny. Modelling and Verification of Timed Interaction and Migration. Lecture Notes in Computer Science, vol. 4961, 215-229, 2008.

[L6] L. Ciortuz, D. Pasailă, I.Mohorianu, „Using base pairing probabilities for microRNA identification”, in Proceedings of the 10th Workshop on Natural Computing and Applications, SYNASC, Timişoara, 2008.

Lucrari in curs de aparitie:
[L7] O. Andrei, D. Lucanu, "Strategy-Based Proof Calculus for Membrane Systems", trimisa spre publicare la Electronic Notes in Theoretical Computer Science.
[L8] D. Lucanu, "Rewriting Logic-based Semantics of Membrane Systems and the Maximal Concurrency", trimis spre publicare la “International Journal of Foundations of Computer Science”.
[L9] G. Ciobanu, M. Gontineac, “Encodings of Multisets”, trimisă pentru publicare la International Journal of Foundations of Computer Science (IJFCS).

[L10] Cosmin Bonchis, Cornel Izbasa, Gratiela Ghergu, Gabriel Ciobanu. Data compression on multisets IeAT Report no, 08-20, 2006 http://www.ieat.ro:8080/IeAT/research/researchreports/msc.pdf/download

[L11] G. Ciobanu (Ed.). Proceedings of 2nd International Meeting on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC), 2008.

Structura si functionarea celulei vii au inspirat doua modele computationale recente: calculul membranar [5] si calculul „brane” [1]. Cele doua modele au doua tinte diferite: pe de o parte sistemele membranare urmaresc o investigare formala a puterii de calcul a membranelor, iar pe cealalta parte, calculul „brane” urmareste sa realizeze o interpretare fidela si cat mai intuitiva a realitatilor biologice.

In lucrarea [L2] am realizat o scufundare a unui fragment al calculului „brane” bazat pe operatiile Pino, Phago si Exo in modelul sistemelor membranare cu obiecte pe suprafata. Aceste sisteme sunt inspirate din fuziunea celulelor, proces prin care o membrana isi incorporeaza obiectele sale intr-o alta membrana; procesul are loc pe baza interactiunii intre proteinele ambelor membrane, ce formeaza complexe stabile.

Sistemele membranare cu obiecte pe suprafata sunt date de un alfabet A, o structura membranara cu cel putin 2 membrane μ,multiseturi de obiecte asociate suprafetei fiecarei membrane, si au reguli diferite de cele des intalnite, de rescriere. Obiectele (de tip a) si co-obiectele (de tip ) sunt cele care controleaza miscarea membranelor. Regulile de evolutie pot fi de trei tipuri:

report08VII_02

Pentru astfel de sisteme am demonstrat ca este decidabil daca se poate ajunge la o anumita distributie de multiseturi pornind de la distributia initiala. Am obtinut acest rezultat prin reducerea la o problema similara din retele Petri.

Trecand la fragmentul de calcul „brane” cu operatii pino, phago, exo (numit calculul PEP), in acesta membranele sunt modelate de compuneri de secvente de actiuni, iar interactiunile intre membrane sunt modelate de actiuni, de obicei complementare.

report08VII_03

Evolutia unui sistem in cadrul PEP este data de urmatorul sistem tranzitional:
report08VII_04

Actiunea pino(p) creeaza o noua membrana interioara ce inlocuieste actiunea pino. In cazul in care doua membrane se ating intr-un punct, actiunea exo si co-actiunea modeleaza reuniunea lor. Actiunea si co-actiunea modeleaza consumarea membranei P de catre membrana Q.

Codarea calculului PEP este data de urmatoarea translatare:

report08VII_09

unde functia S transforma actiuni in obiecte de pe suprafata membranelor, dupa cum urmeaza:

report08VII_10

Tot aceasta functie este folosita si pentru a crea regulile sistemului membranar nou obtinut. Utilizam relatii de congruenta atat intre membrane cat si intre elementele calculului PEP care denota faptul ca unele componente sunt rearanjate pentru a putea interactiona. Am demonstrat corectitudinea translatarii printr-o serie de teoreme: in primul rand, daca M=T(P) iar P este congruent cu Q atunci exista un sistem N congruent cu M astfelincat N=T(Q). Reciproc, daca M este congruent cu N atunci exista Q congruent cu P astfel incat N=T(Q). Mai mult, daca P evolueaza la R in cadrul calculului PEP atunci exista un sistem U incat U=T(R) si M evolueaza la U ca sistem membranar cu obiecte pe suprafata. Reciproc, daca M evolueaza la U atunci exista R incat U=T(R) si P evolueaza la R in cadrul calculului PEP. Consecinta acestor rezultate este ca sistemele membranare cu obiecte pe suprafata au aceeasi putere de calcul ca si calculul PEP. Aceste rezultate confirma intuitia data de similaritatea numelor actiunilor si numelor tipurilor de reguli. In finalul lucrarii deschidem o discutie despre astfel de sisteme membranare in care regulile aplicate sa fie localizate la o singura membrana, spre deosebire de cazul actual in care regulile se pot aplica oricarei membrane in care sunt indeplinite conditiile de aplicare.

Rezultatele etapei si gradul de realizare a obiectivelor

Prin publicarea in reviste cotate ISI sau prezentarea la conferinte de rang inalt am indeplinit toate obiectivele propuse in aceasta perioada in cadrul proiectului ForMol.

Etape/ Activitati/ Parteneri	Grad de indeplinire/activitate	Grad de indeplinire/etapa
Etapa VI. Reţele moleculare cu tipuri şi timp.
Activitatea VI.2 Un formalism cu timp şi tipuri pentru coordonarea reţelelor moleculare. Specificare lanţuri de interacţiuni în KGML. Model checking în P sisteme. Implementarea de functii eficiente de pattern matching flexibil pe siruri.
P1 (IIT)	100%	100%
P2 (UAIC)	100%	100%
P3 (IeAT)	100%	100%

Tinand cont de toate aceste realizari, putem spune ca activitatea de cercetare din cadrul proiectului ForMol a fost bogata, iar obiectivele pentru a doua jumatate a anului 2008 au fost indeplinite.

In perioda raportata au fost elaborate o serie de studii, articole si prototipuri conform planului de realizare a proiectului.
Obiectivele etapei au fost realizate.
S-au adus contributii originale la cercetarea fundamentala si aplicativa a acestui domeniu, prezentate la conferinte nationale si internationale, publicate in jurnale nationale si internationale de specialitate.
Rezultatele obtinute au fost prezentate si discutate in cadrul seminariilor stiintifice la Institutul de Informatica Teoretica, publicate in rapoarte de cercetare ale Institutul de Informatica Teoretica al Academiei Romana. S-a organizat un atelier de lucru, cu scopul de a discuta eventuale colaborari in domeniul sistemelor membranare.
S-a contribuit la cresterea vizibilitatii cercetarii romanesti in comunitatea stiintifica internationala prin participarea la conferinte, comunicarea rezultatelor proiectului la conferinte nationale si internationale cu impact stiintific mare si colaborarea cu diversi cercetatori din tara sau strainatate din domeniul sistemelor membranare ;
S-a organizat conferinta 2nd International Meeting on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2008), 3-4 septembrie 2008, Iasi, Romania.

Parteneri participanti

Termen planificat/

realizat