Formal Methods Laboratory

În modelarea sistemelor distribuite avem de a face cu accesul la resurse, locaţii, comunicarea dintre procese concurente şi migrarea proceselor între domenii. Având nevoie de constrângeri, am introdus în [L1] si [L3] un formalism denumit tMA, ca o extensie a ambienţilor cu proximităţi, tipuri şi limitări de timp. Constrângerile care apar în acest nou formalism sunt: de timp (adoptând o metodă bazată pe mecanisme de măsurat timpul, numite „timers” şi sincronizare printr-un ceas universal), de acces la resurse (prin introducerea noţiunii de “proximitate” ce delimitează domeniul de interacţiune al fiecărui ambient din sistem) şi de comunicare (prin folosirea unui sistem de tipuri bine pus la punct). Canalele de comunicare şi resurse sunt limitate în timp cu ajutorul unor „timers” ce determină durata maximă de acţiune a acestora. Tipurile sunt folosite să exprime accesul restricţionat la resursele distribuite. Folosind tMA, în [L3] se prezintă un model pentru coordonarea în timp a proceselor distribuite care comunică. Coordonarea este dată de limitările în timp date de „timers”, împreună cu reguli de coordonare. Formal, coordonarea este definită printr-o funcţie de asignare a duratei maxime pentru fiecare acţiune, şi printr-o multime de reguli de coordonare.
Aceste extensii ale ambienţilor mobili nu sunt triviale; modelul obtinut este folosit la descrierea protocolului TCP şi a timpului de viaţă a pachetelor reprezentat prin TTL („time-to-live”). Sistemul de tipuri introdus este folosit pentru a asigura că într-un ambient vor fi acceptate doar mesaje dintr-o anumită clasă, astfel încât să fie asigurată buna funcţionare a întregului sistem.
În [L2,L6,L12,L13,L14] s-a arătat că se poate stabili o legătură între ambienţii mobili şi sistemele membranare cu membrane mobile, adică dintre două modele fundamentale utilizate frecvent pentru a modela diverse aspecte ale sistemelor distribuite, modele care se considerau a fi diferite. În [L14] a fost realizată translatarea ambienţilor mobili în sistemele membranare (P sisteme); sistemele membranare reprezintă un formalism inspirat din biologie care implică paralelism şi distribuirea resurselor. Acest lucru a fost realizat prin introducerea unui sistem special de reguli care operează asupra membranelor. În [L2] s-a arătat că este decidabil pentru o clasă specială de sisteme membranare cu membrane mobile, dacă se poate obţine o anumită configuraţie a sistemului pornind de la o configuraţie dată. Pentru demonstrarea acestei proprietăţi a fost folosită o translatare o sistemelor membranare în ambienţii mobili.
            În [L7] se defineşte sistemul tranziţional probabilistic pentru un sistem membranar dat. Deoarece comportamentul sistemelor membranare este în esenţă nondeterministic, se consideră sistemele tranziţionale care efectuează alegeri atât probabiliste cât şi nondeterministe. Probabilităţile sunt adăugate la nivelul regulilor şi ţintelor lor. Pentru aceasta, s-a extins sintaxa şi semantica operaţională a sistemelor membranare cu probabilităţi. Sistemul tranziţional probabilistic corespunzător unui sistem membranar este definit peste configuraţiile acestuia, iar atingerea unei configuraţii este definită ca o secvenţă de tranziţii probabiliste. Abordarea este nouă prin faptul că se iau în considerare combinaţiile posibile ale regulilor aplicabile la un pas în funcţie de resursele disponibile, gradul de consumare a resurselor curente la un astfel de pas de calcul, precum şi probabilitatea de trimitere a mesajelor în regiunile specificate de ţintele corespunzătoare ale regulilor.
În lucrarea [L8], care este o versiune revizuita si extinsă a lui [L18], am studiat structuri de evenimente [6,7] pentru sisteme membranare, luînd în calcul atât relaţiile de cauzalitate cît şi relaţiile de conflict. Sistemele membranare [5] descriu un mecanism computaţional inspirat din biologia moleculară. Structurile de evenimente sunt modele formale definite pentru sisteme paralele şi nedeterminste. Folosirea acestor structuri ne permite să stabilim în manieră formală cînd şi unde anume apar paralelismul şi nedeterminismul în sistemele mebranare.
Am investigat modul în care o structură de evenimente poate fi pusă în corespondenţă cu un pas din procesul de evoluţie paralelă. Concluzia noastră este că semnificaţia unui eveniment depinde de structurile algebrice folosite pentru exprimarea conţinutului membranelor: şiruri sau multiseturi. În cazul folsirii multiseturilor, comutatitvitatea introduce anumite cauzalităţi "false" care trebuiesc înlăturate pentru a se putea exprima paralelismul din sistemele de mebrane. Construcţia structurilor de evenimente pentru cazurile de priorităţi şi promotori poate fi redusă la cazul rescrierii paralele maximale.
Coinducţia circulară este o metodă automată de demonstraţie pentru echivalenţele comportamentale ce poate fi utilizată cu succes la verificarea comportamanetală a sistemelor membranare. Cum nu există niciun algoritm complet pentru demonstrarea echivalenţei comportamentale în general, cea mai eficientă metodă constă în explorarea de euristici sau de reguli de deducţie care să demonstreze egalitatea sau inegalitatea peste şiruri, şi să funcţioneze corect peste exemple particulare, de interes. CIRC conţine un set de reguli de rescriere care implementează principiul circularităţii. Eficienţa demonstratorului CIRC poate fi sporită prin adăugarea de noi proprietăţi, implementate de asemenea cu reguli de rescriere. De asemenea, CIRC permite într-un cadru limitat efectuarea unor demonstraţii inductive automatizate, care pot fi utilizate alături de coinducţie.
Lucrarea [L23] a fost prezentată în cadrul conferinţei "7th International Workshop on Reduction Strategies in Rewriting and Programming". Lucrarea dovedeşte corectitudinea demonstratorului coinductiv şi prezintă modalitatea prin care strategiile de rescriere, exprimate sub formă de expresii regulate, pot fi utilizate în specificarea tehnicilor de demonstrare pentru CIRC. În lucrare se defineşte o tehnică de demonstrare care combină coinducţia circulară cu o formă particulară de simplificare, în scopul probării echivalenţei proceselor independente de context. Pentru a exprima tehnica de demonstrare, s-a utilizat un limbaj de strategie bazat pe expresii regulate. CIRC include o specificare comportamentală a expresiilor regulate, în scopul manipulării tehnicii de demonstrare.
            Utilizarea strategiilor regulate ca tehnici de demonstrare lărgeşte clasa problemelor ce pot fi rezolvate automat. CIRC implementează de asemenea principiul circularităţii în demonstrarea proprietăţilor prin inducţie. Strategiile regulate folosesc tehnici de demonstraţie care combină coinducţia cu inducţia. Acest lucru se poate realiza momentan doar cu intervenţia utilizatorului.
Lucrarea [L22] a fost prezentată în cadrul conferinţei "9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing". Această lucrare include o extindere a CIRC, adăugând capacitatea de a demonstra comutativitatea comportamentală. Eficienţa versiunii extinse a demonstratorului este ilustrată printr-un exemplu de calcul coinductiv pe şiruri. În acest sens se aduc două contribuţii majore: se extinde CIRC cu abilitatea de a demonstra comutativitatea comportamentală a operaţiilor de tipul _+_ peste şiruri şi se automatizează demonstrarea proprietăţilor de interes pentru şiruri. Chiar dacă proprietatea de comutativitate este elementară, tratarea ei în cadrul motoarelor de rescriere s-a dovedit a fi o sarcină dificilă.
Rescrierea modulo asociativă şi comutativă este o problemă NP-dificilă, dar exista algoritmi eficienţi pentru cazurile practice şi majoritatea motoarelor de rescriere îi adoptă. Se demonstrează că rescrierea modulo comutativă poate fi folosită cu succes în scopul manipulării comutativităţii comportamentale în multe exemple practice, dat fiind faptul că operaţiile peste stări sunt congruente din punct de vedere comportamental. De asemenea se prezintă modalităţi prin care axiomele comportamentale pot fi utilizate pentru demonstrarea altor proprietăţi. Pe viitor, unul dintre obiectivele CIRC se referă la demonstrarea echivalenţei programelor în urma extinderii acestui limbaj.
În [L17] s-a introdus reţelele de automate multiset Mealy, arătînd că în ce priveşte puterea lor computaţională, ele sunt complete, întrucât o reţea multiset Mealy este capabilă să simuleze o maşină Turing. Cercetările recente [1] folosesc teoria automatelor ca un mijloc eficient de descriere şi control a activităţii genelor. O secvenţă ADN este modelată ca un mic automat care apoi este folosit pentru controlul logic al exprimării genei reprezentată de secvenţa respectivă.
A fost investigată o modalitate de interacţiune dintre gene şi proteine (şi anume procesul producerii proteinelor) în termeni de automate Mealy, semigrupuri de transformare şi operaţii abstracte. Automatul Mealy propus ca model formal pentru traducerea mesajului genetic este unul minimal, acceptând mesajele mARN şi terminând procesul de traducere.
Totuşi biologia moleculară are de a face nu doar cu secvenţe ci şi cu multiseturi. [4] introduce şi studiază automate multiset, maşini care lucrează asemenea automatelor dar generează-recunosc nu secvenţe ci multiseturi. Un automat multiset Mealy poate fi văzut în mod corespunzător ca o maşină Mealy. Pentru a defini reţelele de automate multiset Mealy conectăm aceste automate în diverse moduri, folosind atât conexiuni paralele cât şi conexiuni seriale. În [3] am definit produsul direct restricţionat de automate multiset Mealy pentru cazul paralel, precum şi produsul în cascadă pentru conexiuni seriale.
Pentru a obţine puterea de calcul a unei reţele de automate multiset Mealy, facem corespondenţa cu sisteme neuronale P, demonstrând că aceste reţele sunt complete din punct de vedere computaţional.
Lucrarea [L21] introduce o nouă modalitate de învăţare automată a funcţiilor nucleu pentru maşini cu vectori suport (SVMs), folosind tehnici de programare genetică (GP). Algoritmul propus, InfoBoosted GP, realizează o extindere a algoritmului InfoBoost (care la rîndul său este o imbunătăţire a bine-cunoscutului meta-algoritm de învăţare automată AdaBoost) cu un modul GP care este responsabil de propunerea şi testarea de noi funcţii nucleu, pornind de la funcţii nucleu elementare de tip RBF (funcţii cu baza radială).
Ideea de bază a algoritmului InfoBoosted GP este următoarea: Se cunoaşte deja că adunarea, înmulţirea şi înmulţirea cu un număr real sunt operaţii interne pe mulţimea funcţiilor nucleu. În consecinţă, în InfoBoosted GP aceşti operatori servesc în mod direct la propunerea de funcţii nucleu, alături de operatorii genetici de tip mutaţii, ştergeri sau combinaţii cromozomiale. Validarea funcţiilor nucleu nou-propuse se face pe un eşantion ales din setul de date de antrenament, în aşa fel încât învăţarea se concentrează în runde succesive pe date din ce în ce mai dificil de tratat. Implementarea algoritmului InfoBoosted GP a fost facută utilizând sistemele open-source ECJ (Evolutionary Computing in Java) şi libSVM de la Universitatea din Taiwan.
Algoritmul InfoBoost GP a fost testat pe trei baze de date din cadrul UCI Repository şi pe o bază de date pentru clasificarea de proteine furnizată nouă de către colegi de la Universitatea din Marsilia, Franţa. Rezultatele testării arată că algoritmul Infoboosted GP este (pe aceste cazuri) mai bun decât învăţarea de funcţii nucleu bazată doar pe programare genetică. În viitor vom explora posibilitatea aplicării algoritmului Infoboosted GP la învăţarea de funcţii nucleu pentru SVM-urile folosite la identificarea de microRNA-uri (vezi [L20]) şi pe SVM-urile pentru identificarea de site-uri target pentru microRNA-uri.
Lucrarea [L20] face o prezentare state-of-the-art în domeniul identificării de microRNA-uri cu ajutorul metodei SVM (Support Vector Machine), care este la ora actuală probabil cea mai des folosită metodă de învăţare automată de tip discriminativ. MicroRNA-urile au fost decoperite în ultima decadă şi alături de alte categorii de RNA non-codant constituie o clasă de secvenţe gentice care suscită astăzi un interes major din partea cercetătorilor din biologie moleculară, genetică şi medicină, datorită fenomenului de interfenţă mediată RNA (pe scurt, interferenţă RNA) pe care îl generează. Acest fenomen constituie o excepţie de la bine-cunoscuta dogmă centrală a biologiei moleculare: DNA ® RNA ® proteine. Prin interferenţă RNA se blocheză procesul de transformare (translatare) a RNA-ului mesager în proteine. Acest proces se poate aplica pentru identificarea funcţiilor genelor (prin knock-out), cu aplicaţie la studiul producerii cancerului.
Există o bază de date publică, numită miRBase, care cataloghează toate secvenţele microRNA identificate pînă în prezent şi care au fost verificate în laborator (sau sunt omoloage cu secvenţe verificate în laborator). Este foarte util ca plecând de la această bază de date să se poată identifica/propune noi secvenţe microRNA, pentru a limita costurile de timp şi financiare necesitate de verificările în laborator. SVM-urile (şi în general învăţarea automată) constituie un bun candidat la rezolvarea acestei probleme, fiindcă metodele clasice de comparare a secvenţelor nu sunt foarte utile în acest caz, întrucât structura primară a RNA-urilor în general nu este bine conservată de la o specie la alta.
            Lucrarea [L20] este după cunoştinţa noastră singura lucrare la ora actuală care face o sinteză a SVM-urilor existente pentru identificare de microRNA-uri. Ea prezintă asemănări şi deosebiri între seturile de trăsături/caracteristici folosite de diferitele SVM-uri, proceduri de selecţie de trăsături folosite, performanţele SVM-urilor pe diferite seturi de date, precum şi extensii/altenative ale acestor clasificatori. Lucrarea poate servi ca un bun punct de plecare pentru învăţarea de funcţii nucleu pentru aceste SVM-uri, cu scopul înbunătăţirii performanţelor lor.
Liviu Ciortuz a fost invitat să lucreze în perioada 10 iunie - 27 iulie la “Institute National de Recherche en Intelligence Artificielle” (INRIA), Lille, în cadrul echipei de Bioinformatică condusă de Dr. Gregory Kucherov şi Dr. Helene Touzet. În timpul acestei şederi el a studiat clasele funcţii nucleu pe şiruri folosite recent în problemele de remote homology detection şi protein fold recognition. Colabo-rarea cu echipa de Bioinformatica de la Lille a dus la acceptarea la studii de doctorat a Martei Gîrdea, absolventă a programului de master în cercetări operaţionale la Facultatea de Informatică din Iaşi.
De asemenea, Liviu Ciortuz a efectuat un stagiu de cercetare în perioada 27 iunie – 18 august 2007, la Biozentrum, Swiss Institute for Bioinformatics, University of Basel, Elveţia. El a studiat şi discutat cu Prof. Dr. Mihaela Zavolan şi Prof. Dr. Erik van Nimwegen în legătură cu tehnicile de învăţare automată discriminative, în speţă masinile cu vectori-support (SVM), aplicate la clasificarea secvenţelor microARN. Lucrarea [L21] este urmarea directă a acestor două stagii de cercetare efectuate de Liviu Ciortuz în străinătate în cursul anului 2007. În afara simpozionului EHB'07, această lucrare a mai fost prezentată şi la Departamentul de Matematică al Universităţii "Lucian Blaga" din Sibiu, in data de 7 noiembrie 2007.
In [L5] sunt studiate aspecte de compozitionalitate a P sistemelor, lucrare fiind inspirata de teoria procesoarelor asincrone. Se contureaza mecanisme teoretice pentru cuplarea asincrona a P sistemelor computationale, folosind handshake-uri implementate prin reguli antiport si cu promotori. Prin folosirea regulilor antiport din teoria P sistemelor am obtinut un protocol de comunicare simplificat in comparatie cu protocoalele existente in teoria procesoarelor asincrone.
            Pornind de la teoria Shannon a informatiei, in lucrarea L[15] am prezentat cazul producerii informatiei sub forma de multiseturi si de asemenea codificarea informatiei utilizand multiseturi. Am revizuit rata entropiei unei surse de informatie ce produce multiseturi si am determinat o formula pentru calcularea continutului informational a unui multiset. Tot in aceasta lucrarea au fost studiate codificatorul si capacitatea canalului sistemului unde am obtinut rezultate referitoare la lungimea codificarii pe multiset si de capacitatea canalului.

[L1] B.Aman, G.Ciobanu. Mobile Ambients with Timers and Types. Lecture Notes in Computer Science, vol 4711, 50-63, 2007.

[L2] B.Aman, G.Ciobanu. Reachability Problem in Mobile Membranes, Lecture Notes in Computer Science, vol 4860, 113-123, 2007.

[L3] B.Aman, G.Ciobanu. Timers and Proximities for Mobile Ambients. Lecture Notes in Computer Science, vol 4649, 33-43, 2007.

[L4] O.Andrei, G.Ciobanu, D.Lucanu. A rewriting logic framework for operational semantics of membrane systems. Theoretical Computer Science vol.373, 163-181, Elsevier, 2007.

[L5] C. Bonchis, C. Izbasa, G. Ciobanu. Compositional asynchronous membrane systems. Progress in Natural Science vol.17(4), 411-416, 2007.

[L6] G.Ciobanu, B.Aman. On the relationship between membranes and ambients, BioSystems(2007). doi:10.1016/j.biosystems.2007.01.006

[L7] G.Ciobanu, L.Cornacel. Probabilistic transitions for P systems. Progress in Natural Science vol.17(4):432-441, 2007.

[L8] G.Ciobanu, D.Lucanu: Event Structures for Membrane Systems, Lecture Notes in Computer Science, vol 4860, 209-227, 2007.

[L9] G.Ciobanu, Linqiang Pan, Gh.Paun, M.Perez-Jimenez. P Systems with Minimal Parallelism. Theoretical Computer Science vol.378, 117-130, 2007.

[L10] F.J. Romero-Campero, M. Gheorghe, G. Ciobanu, J.M. Auld, M.J. Perez-Jimenez. Cellular modelling using P systems and process algebra. Progress in Natural Science vol.17(4), 375-383, 2007.

[L11] B.Aman, G.Ciobanu. Describing the Immune System Using Enhanced Mobile Membranes, FBTC, Workshop CONCUR, 1-13, 2007.

[L12] B.Aman, G.Ciobanu. Mobile Ambients and Mobile Membranes, Proceedings CiE, 2007.

[L13] B.Aman, G.Ciobanu. Structural Properties and Observability in Membrane Systems, SYNASC, 71-78, 2007.

[L14] B.Aman, G.Ciobanu. Translating Mobile Ambients into P Systems. Electronic Notes in Theoretical Computer Science, vol 171(2), 11-23, 2007.

[L15] C.Bonchis, C.Izbasa, G.Ciobanu. Information Theory over Multisets, Proceedings WMC8, 165-172, 2007.

[L16] G.Ciobanu. Time and Space Coordination of Mobile Agents. Proceeding of the 1st International Symposium on Intelligent and Distributed Computing, Springer, 9-24, 2007.

[L17] G.Ciobanu, M.Gontineac. Networks of Mealy Multiset Automata, Proceedings WMC8, 243-254, 2007.

[L18] G.Ciobanu, D.Lucanu: What is an event for membrane systems, Proceedings WMC8, 255-266, 2007.

[L19] G.Ciobanu, C.Prisacariu. Coordination by Timers for Channel-Based Anonymous Communications. Electronic Notes in Theoretical Computer Science, vol 175(2), 3-17, 2007.

[L20] L. Ciortuz. Support Vector Machines for MicroRNA Classification. Revista Medico-chirurgicală a Universităţii de Medicină “Gr.T. Popa” Iaşi, Proceedings of EHB'07, The Workshop on E-Health and Bio-Engineering, Iaşi, România, 2007.

[L21] M. Girdea, L. Ciortuz. A Hybrid Genetic Programming and Boosting Technique for Learning Kernel Functions from Training Data.The Natural Computing and Application (NCA) Workshop, held in conjunction with the 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'07), Timişoara, România, 2007.

[L22] D. Lucanu. Proving behavioral commutativity with CIRC. 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'07), Timişoara, România, 2007.
[L23] D. Lucanu, G. Roşu, Gh. Grigoraş. Regular Strategies as Proof Tactics for CIRC Prover. 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007. To appear in ENTCS.

In perioada raportata au fost elaborate si alte studii stiintifice si tehnice ale activitatilor cuprinse in planul general al proiectului. Cercetarile actuale au continuat si consolidat rezultate precedente precum au si deschis linii noi de cercetare.
Sistemele membranare reprezinta un model abstract nou inspirat din compartimentarea celulelor si de membranele moleculare. Un astfel de sistem mai este numit si P sistem.El se compune din mai multe compartimente, fiecare compartiment avand un task diferit, si toate impreuna lucrand simultan pentru a realiza un task mult mai general al intregului sistem.
In [L11] extindem sistemele membranare cu membrane mobile cu noi reguli de evolutie si folosim aceasta noua clasa de sisteme membranare pentru a modela unele evolutii in sistemul imunitar.
Aceasta noua clasa de membrane mobile este definita in felul urmator:

07501
07502 07503
07504

Regulile de tip c) si d) sunt folosite pentru a simula miscarea membranelor sub controlul unor obiecte din interiorul lor, pe cand regulile de tip e) si f) simuleaza miscarea membranelor sub controlul unor obiecte aflate in membranele pe care le tranziteaza. De asemenea, un nou tip de reguli, anume b), exprima faptul ca un obiect dintr-o membrana poate evolua doar in prezenta unui alt obiect dintr-o membrana vecina. Exemplul pe care l-am considerat in lucrare este urmatorul: modul in care celule dendritice protejeaza corpul uman impotriva infectiilor.

07505

Pentru a simula evolutia din figura de mai sus, toate componentele sistemului imunitar vor fi reprezentate in sistemele membranare dupa cum urmeaza:

O celula dendritica imatura care doreste sa manance orice bacterie pe care o intalneste este reprezentat de o membrana DC care contine un obiect eat folosit pentru a captura bacteria. Imediat ce celula dendritica se maturizeaza, obiectul eat este consumat.

O bacterie va fi reprezentata ca o mebrana bacterium care contine un obiect antigen care contine informatia bacteriei.

Nodul limfatic este locul unde celule dendritice se maturizeaza pentru a putea migra la locul infectiei pentru a putea lupta impotriva bacteriilor.

07509

Activarea celulelor dendritice duce la activarea a doi noua tipuri de celule, anume celule T si celule B, care sunt codate in modsimilar:

Acest exemplu motiveaza introducerea noi clase de membrane mobile; mai exact motiveaza noile reguli introduse si modul in care acestea sunt folosite pentru a modela unele sisteme biologice. Ar fi foarte folositoare cautarea de noi exemple care sa poata fi modelate cu aceasta noua clasa de sisteme membranare.
Lucrarea se termina cu o incercare de formalizare a clasei de membrane mobile introdusa mai sus.

07512

Semantica operationala a sistemelor membranare este definita in modul urmator:

07513

Aceste reguli de evolutie sunt utilizate pentru a modela evolutia sistemul imunitar modelat anterior.

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 IV. Teoria şi practica P sistemelor.
Activitatea IV.2 Studiul teoretic cu privire la paralelismul maximal, executie nedeterminista si reprezentarea datelor. P sisteme pentru modelarea unei biounitati aritmetice si logice. Simulator software de P sisteme. Şi adaptarea la standardul SBML.
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 2007 au fost indeplinite.

Parteneri participanti

Termen planificat/

realizat