Formal Methods Laboratory

Se vor cuantifica indicatorii adecvati, de tipul celor din lista, care au fost urmariti in realizarea fazei curente a proiectului:

Tabel centralizator privind estimarea cuantificarii
indicatorilor de monitorizare si evaluare pe Etapa nr. I a proiectului

O1. Introducerea si studierea unor structuri abstracte care sa exprime interactiunea proceselor biologice celulare.

O2. Crearea unor modele matematice care sa stea la baza calculului paralel si distribuit, oferind in acelasi timp instrumente formale pentru verificarea si determinarea unor proprietati.

           Conform obiectivelor si activitatilor stabilite in cadrul planului proiectului, aceasta faza a proiectului este orientata spre studiu teoretic de realizare a unor structuri abstracte pentru interactiunea proceselor biologice.
            In [L1] am considerat doi parametrii de complexitate in ceea ce priveste graful configuratiilor accesibile dintr-un P sistem, si anume numarul de iesiri ca masura a gradului de nedeterminism si numarul de intrare ca masura a gradului de confluenta. O cercetare a acestor parametrii a fost dusa la bun sfarsit, mai ales in ceea ce priveste decidabilitatea. Cele mai multe rezultate furnizeaza raspunsuri negative in ceea ce priveste decidabilitatea si computabilitatea. Urmeaza a se cerceta cum se pot obtine rezultate pozitive de dicabilitate.
           In [L2] am continuat un studiu inceput anul trecut cu privire la Mealy Membrane Automata. S-au studiat rezultate importante asupra P transducerelor in [L3]. Urmărind o noua abordare, a fost definită o semantică operaţională a unei clase fundamentale de P sisteme care a fost translatată înntr-un sistem de rescriere [L4]. De asemenea, sunt investigate proprietăţilor algebrice şi coalgebrice a P sistemelor [L2,L5,L19]. Abordările topologice în studiul P sistemelor sunt noi, iar obiectivul urmărit constă în utilizarea conceptelor şi rezultatelor topologice pentru a descrie evoluţia celulelor şi obţinerea de rezultate predictive privind evoluţia acestora.
O atenţie deosebită este acordată operaţiilor cu membrane (dizolvare, fuziune, scindare, multiplicare, exo şi endo), in paralel cu operatiile cu obiecte din membrane. Rezultatele obţinute ne îndreptăţesc să credem ca instrumentele şi metodele matematice folosite pot fi utilizate si pentru investigarea altor modele de calcul.
Alte rezultate interesante asupra sistemelor membranare au fost prezentate in [L6,L9] unde se prezinta un mod de codificare a numeralelor si a operatiilor asociate (ca adunarea sau inmultirea) cu acest formalism de sisteme membranare. Astfel, in [L6] am tratat cateva codificari ale numerelor peste multiseturi. Am prezentat codificarea naturala si cea mai compacta codificare, si am studiat proprietatile acestor codificari folosind elemente din combinatorica peste multiseturi. Am construit sisteme membranare care implementeaza operatiile aritmetice peste codificarile prezentate. Pentru fiecare codificare si operatie descrisa am prezentat si explicat complexitatile. Privind complexitatea, am comparat codificarile si s-a remarcat faptul ca s-a ajuns, spre deosebire de lungimea si complexitatea codificarii pe stringuri, la o lungime a codificarii log b (n) si la o complexitate de ordinul “radical de ordinul b din n“. Astfel de rezultate sunt necesare pentru a incepe un studiu detaliat asupra unei masini de calcul bazata pe sisteme membranare (asa cum sunt si calculatoarele obisnuite).
           Time Distributed pi-calculus (TDpi) este un calcul introdus de noi in [L10] ca o extensie cu timp, tipuri si locatii a pi-calculului. Este conceput pentru a modela sisteme distribuite de o mare complexitate si cat mai apropiate de cele din realitate. In acest sens am oferit posibilitatea modelarii unei game largi de restrictii cum ar fi restrictiile de timp (adoptand o metoda bazata pe timere si sincronizare printr-un ceas universal), restrictii de acces la resurse si restrictii de comunicare (realizate cu ajutorul unui sistem de tipuri bine pus la punct), precum si modelarea migrarii proceselor intre locatiile sistemului distribuit. Acest calcul este demonstrat a fi consistent. Se demonstreaza si faptul ca trecerea timpului nu afecteaza sistemul de tipuri. Un model de coordonare in functie de timp este introdus. Modelul clasic de sistem distribuit la care aplicam acest nou calcul este reteaua moleculara. In [L22] este studiat mai in amanunt acest calcul si se dau diverse rezultate teoretice.
           In sistemele dinamice, aspectele cantitative referitoare la comportamentul acestora sunt importante si merita sa fie studiate. Astfel, in [L11] am extins sintaxa si semnatica pentru fusion calculus la stochastic fusion calculus, dinamica unui sistem fiind descrisa de distributii de probabilitate. Am studiat numai cazul in care distributia de probabilitate este functia exponentiala, urmand ca in viitor sa tratam si alte cazuri si sa aplicam aceste rezultate in sistemele membranare.
           De asemenea, ne-am indreptat atentia asupra altor formalisme inspirate din biologie cum ar fi Mobile Ambients (ambientii mobili) in [L14,L21].
Folosindu-ne de cunostiintele furnizate de teoria programarii, in [L7] prezentam sintaxa si semantica sistemelor membranare. Definim astfel multimea de reguli de inferenta corespunzatoare a trei pasi in evolutia sistemelor membranare. Este definita si relatia de bisimilaritate pentru a compara comporatamentul dinamic a doua sisteme membranare.
           In [L24] se defineste sistemul tranzitional probabilistic pentru un sistem membranar dat. Deoarece comportamentul sistemelor membranare este in esenta nondeterministic se considera sistemele tranzitionale care efectuaza alegeri atat probabiliste cat si nondeterministe. Probabilitatile sunt adaugate la nivelul regulilor, tintelor si dizolvarii membranelor. Pentru aceasta, s-a extins sintaxa si semantica structurala operationala a sistemelor membranare [L7] cu probabilitati. Sistemul tranzitional probabilistic corespunzator unui sistem membranar este definit peste configuratiile acestuia, iar obtinerea unor noi configuratii este definita ca o secventa de tranzitii probabiliste dintre configuratii. Pentru a simula un sistem membranar cu probabilitati s-a construit si un simulator in Matlab bazat pe sintaxa si semantica definite pentru sistemele membranare. De asemenea, pentru verificarea unor propietati se poate folosi PRISM, un model checker probabilistic.
           In [L28] s-au inclus P sistemele corespunzatoare operatiilor aritmetice pentru codificarile in baza 1, 2 si 3 si sunt prezentate documentele XML asociate fiecarui P sistem, testate si simulate cu ajutorul simulatorului nostru: http://psystems.ieat.ro.

Lucrari publicate, produse concepute/omologate (dupa caz):

Lucrari ISI

L1. G.Ciobanu, Gh.Paun, M.J. Perez-Jimenez. On the branching complexity of P systems. Fundamenta Informaticae vol.72, 1-11, 2006.
L2. G.Ciobanu, V.M.Gontineac. Mealy Multiset Automata. International Journal of Foundations of Computer Science vol.17, 111-126, 2006.
L3. G.Ciobanu, Gh.Paun, Gh.Stefanescu. P Transducers. New Generation Computing, vol.24(1), 1-28, 2006.

L4. O.Andrei, G.Ciobanu, D.Lucanu. Operational Semantics and Rewriting Logic in Membrane Computing. Electronic Notes in Theoretical Computer Science. vol.156, 57-78, 2006.

L5. G.Ciobanu, M.Gontineac. Algebraic and Coalgebraic Aspects of Membrane Computing. WMC 2005, LNCS 3850, Springer, 182-199, 2006.

L6. C.Bonchis, G.Ciobanu, C.Izbasa. Encodings and Arithmetic Operations in Membrane Computing. In: Jin-Yi Cai, S.Barry Cooper, Angsheng Li (Eds.): Theory and Applications of Models of Computation, LNCS 3959, Springer, 618-627, 2006.

L7. O. Andrei, G. Ciobanu, D. Lucanu. Structural Operational Semantics of P Systems. Proceedings WMC6, LNCS vol.3850, Springer, 32-49, 2006.

L8. G.Ciobanu, D.Rusu, Algebraic and Topological Properties of Apartness Lattice-Ordered Semigroups, Journal of Multiple-Valued Logic and Soft Computing, vol. X, , 1-26, 2006.

Lucrari IEEE sau ACM:

L9. G. Ciobanu. Theory and Practice of Programming Applied to Membrane Systems. Invited talk. In Proceedings 7th SYNASC Conference, IEEE Computer Society, 19-25, 2006.

Lucrari in alte publicatii nationale/internationale

L10. G.Ciobanu, C.Prisacariu. Timers for Distributed Systems. In Proceedings of 4th Workshop on quantitative Aspects of Programming Languages (QAPL), 56-73, 2006

L11. G.Ciobanu, L.Cornacel. Stochastic Fusion Calculus, In Proceedings of 4th Workshop on quantitative Aspects of Programming Languages (QAPL), 109 - 125, 2006 .

L12. G.Ciobanu, D.Lucanu. Communicating concurrent objects in hiddenCCS. Electronic Notes in Theoretical Computer Science, vol.117, 353-373, 2005

L13. G.Ciobanu. A Programming Perspective of the Membrane Systems. Invited talk. Proceedings of ICCCC, Editura Univ.Agora, 13-22, 2006.

L14. B.Aman, G.Ciobanu. Translating Moblie Ambients into P Systems. N.Busi, C.Zandron (Eds.): Proceedings of Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC’06), 14-30, 2006.

L15. O.Andrei, G.Ciobanu, D.Lucanu. Expressing control mechanisms by rewriting strategies. Proc. of Workshop on Membrane Computing (WMC7), Lorentz Center Leiden, p.119-131, 2006.

L16. G.Ciobanu, M.Gontineac: "P Machines: An automata approach of membrane computing" Proc. of Workshop on Membrane Computing (WMC7), Lorentz Center Leiden, p.274-289, 2006.

L17. G.Ciobanu, D.Zaharie: "Distributed evolutionary algorithms inspired by membranes in solving continuous optimization problems", Proc. Workshop on Membrane Computing (WMC7), Lorentz Center Leiden, p.522-537, 2006.

L18. G.Ciobanu, V.Zakharov. Encoding mobile ambients into pi-calculus. InProc. Perspectives of System Informatics, Novosibirsk, 79-90, 2006.

L19. M. Gontineac, Mealy Membrane Automata: An Automata-like Approach of Membrane Computing, Proc. of the Int. Conf. on Computers, Communications & Control, June 1-3, Oradea, Romania, 2006, 222-228.

Rapoarte tehnice

L20. B. Aman and G. Ciobanu. On the Relationship Between P Systems and Mobile Ambients, Technical Report, ISSN 1842 - 1490, May 2006.

L21. C. Prisacariu and G. Ciobanu. Technical Aspects of Timed Distributed pi-calculus, Technical Report, ISSN 1842 - 1490, May 2006.

Thesis

L24. L. Cornacel. Probabilistic aspects of formalisms inspired from biology. Master thesis, "A.I.Cuza" University of Iasi, June 2006.

Books

L25. G. Ciobanu, Gh.Paun, M.J.Perez-Jimenez (Eds.): Applications of Membrane Computing, Natural Computing Series, x+439p., Springer, 2006.

L26. D.Zaharie, D.Petcu, V.Negru, T.Jebelean, G.Ciobanu, A.Cicortas, A.Abraham, M.Paprzycki (Eds.): Proceedings SYNASC 2005, IEEE Computer Society, 2006.

L27. G.Ciobanu, D.Rusu, Metrics over Synch Resource Algebra, submitted 2nd International Conference on Intelligent Computer Communication and Processing (ICCP’06), 2006.

L28. A. Alhazov, Cosmin Bonchis, Cornel Izbasa, Gabriel Ciobanu. Encodings and Arithmetic Operations in Membrane Computing. Submitted.

L29. G. Ciobanu, L. Cornacel. Probabilistic Transitions for P Systems. Submitted to Bio-Inspired Computing: Theory and Applications (BIC-TA), September 18-22, 2006, Wuhan, China.

L30. Cosmin Bonchis, Cornel Izbasa, Gabriel Ciobanu. Compositional Asynchronous Membrane Systems. Submitted to Bio-Inspired Computing: Theory and Applications (BIC-TA) September 18-22, 2006, Wuhan, China.

L31. O.Andrei,G.Ciobanu,D.Lucanu, A Rewriting Logic Framework for Operational Semantics of Membrane System, Preprint submitted to Elsevier Science.

L32. D. Lucanu, New challenges for rewriting engines provided by implementation of membrane systems, Formal Methods Laboratory, University of Illinois at Urbana-Champaign, March, 2006.

           In perioada raportata au fost elaborate studii care indica premisele stiintifice si tehnice ale activitatilor cuprinse in planul de realizare. Cercetarile actuale au continuat si consolidat rezultate precedente precum au si deschis linii noi de cercetare. 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.
Sistemele membranare reprezinta un model abstract nou inspirat din compartimentarea celulelor si de membranele moleculare [L15,L17,L7,L18]. 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.
           Pentru fiecare model abstract, teoria programarii introduce diverse notiuni si paradigme de calcul. De exemplu, masinile Turing si masinile cu registri sunt legate de programarea imperativa, iar lambda-calculul este legat de programarea functionala. Este natural ca si sistemele mebranare sa fie studiate dintr-un punct de vedere al teoriei programarii. Aceasta presupune definirea unei sintaxe abstracte si a semanticii operationale pentru sistemele membranare.
           Semantica operationala structurata (SOS) [14,21] constituie un cadru de lucru excelent pentru descrierea formala a sistemelor. SOS este intuitiva si flexibila, ceea ce i-a permis sa devina foarte atractiva. Un rol deosebit in dezvoltarea acestui domeniu l-au avut G.Plotkin [21], G.Kahn [10], si R.Milner [13].
Noi am reusit sa definim pentru prima data semantica operationala a P sistemelor in termenii SOS [L1]. Semantica definita de noi este de tipul “big step”, fiecare pas reprezentand o colectie de pasi paraleli urmand principiul paralelismului maximal conform caruia o membrana executa in paralel la un moment dat un numar maxim de pasi elementari posibili.
           Sintaxa abstracta pentru P sisteme defineste clar structura ierarhica a sistemului si notiunea de configuratie necesara descrierii calculului. O proprietate caracteristica a P sistemelor este aceea ca descrierea configuratiei include atat descrierile starilor membranelor componente, cat si partea de control pentru fiecare membrana. Partea de control a unui P sistem are un caracter dinamic in sensul ca ea se poate modifica in timpul unui calcul. Aceasta particularitate nu apare la paradigmele de programare clasice in care programul este invariant pe parcursul executiei. Partea de control a unui P sistem consta dintr-un set finit de reguli de rescriere peste multiseturi de resurse.
           Executia unui pas de catre un P sistem consta din trei etape. In prima etapa sunt executate de catre fiecare membrana regulile de evolutie, respectand principiul rescrierii maximal paralele. Acest principiu se aplica numai pentru partea de control a unei membrane; ordinea in care membranele evolueaza nu are importanta, aceasta avand un caracter concurent. In etapa a doua au loc comunicarile intre membranele aflate in relatia parinte-copil. Comunicarile sunt date de mesajele rezultate in prima etapa,iar realizarea lor are un caracter concurent. Ultima etapa a unui pas de calcul consta in dizolvarea membranelor ce contin o resursa speciala notata cu d; aceasta resursa apare ca rezultat al aplicarii regulilor de evolutie. Prin dizolvare, resursele membranei dizolvate sunt transferate in membrana parinte, iar regulile membranei dizolvate dispar. Aceasta etapa confera un aspect dinamic a partii de control a intregului sistem si clasifica P sistemele ca o subparadigma de programare adaptiva. Toate cele trei etape au putut fi descrise formal cu o multime R de reguli de deductie, obtinandu-se astfel o logica pentru P sisteme. Un pas de calcul poate fi descris ca un arbore de decizie. Cu alte cuvinte, configuratia C’ se obtine intr-un singur pas din C daca si numai daca R |= C Þ C’. Implementarile P sistemelor utilizeaza o semantica operationala de tip “small step”. Un pas mare (“big step”) este obtinut ca o secventa de pasi mici (“small steps”). De notat ca in general secventa de pasi mici nu este unica. Un prim pas de definire a unei semantici bazate pe pasi mici a fost facut in [L2], unde s-a dat o codificare a P sistemelor in logica rescrierii (“rewriting logic”) utilizand sistemul Maude [7]. Tot in [L2] s-a aplicat pentru prima data un algoritm de model-checking pentru analiza si verificarea unui P sistem. Totusi, s-a observat ca motoarele de rescriere actuale nu sunt capabile sa ofere mediu adecvat pentru simularea fidela a aspectului (puternic) nedeterminist al P sistemelor.
           Implementarea P sistemelor utilizeaza intensiv rescrierea modulo asociativitate-comutativitate. Se stie ca problema de “AC matching” este NP-completa si din acest motiv orice motor de rescriere utilizeaza un algoritm cat mai eficient de “AC matching”. Pretul platit este pierderea nedeterminsmului: daca pentru o anumita configuratie sunt mai multe posibilitati de continuare a calculului, de fiecare data motorul de rescriere va alege o aceeasi cale. Unul din pasii viitori de cercetare este de a da o descriere a semanticii P sistemelor bazata pe pasi mici independenta de motorul de rescriere. O optiune promitatoare o constituie utilizarea strategiilor de rescriere [25]. O atentie deosebita va fi acordata si implementarii “fair” a nedeterminismului. Pentru analiza si verificarea P sistemelor se vor utiliza atat algoritmii de cautare exhaustiva (cum ar fi ”search” din Maude) cat si algoritmi de model-checking. Pentru aceasta, se simte necesitatea definirii unei logici adecvate pentru descrierea proprietatilor sistemelor membranare.

1) Ambienti si P sisteme

Ambientii si sistemele membranare (care mai poarta denumirea de P sisteme) au structuri similare si concepte comune. Amandoua au o structura ierarhica bazata pe locatii. Ambientii mobili sunt potriviti pentru reprezentarea migrarii proceselor intre anumite locatii; P sistemele descriu evolutia obiectelor si migratia lor intre membrane apropiate.
In cele ce urmeaza consideram aceste doua modele si prezentam translatarea ambientilor mobili in sisteme membranare, fiecare pas al acestei translatii fiind explicat in detaliu in lucrarea [L14,L20].
Pentru a face translatarea ambientilor mobili in P sisteme executam initial urmatorii pasi:

O caracteristica a ambientilor este ca au o structura spatiala de arbore. Nodurile din aceasta structura sunt reprezentate de ambienti si de capabilitati. Cand efectuam aceasta translatare obtinem aceeasi structura spatiala de arbore in sistemul membranar: fiecare nod este o membrana corespunzatoare unui ambient sau unei capabilitati.
Cautam sa definim o multime de reguli care sa asocieze un unic obiect fiecarei capabilitati in asa fel incat ordinea capabilitatilor sa fie conservata. Fiecare capabilitate consumata in ambienti produce o schimbare in structura ambientilor. Simulam aceste operatii in P sisteme cu ajutorul unor reguli speciale. Urmand [11], introducem urmatoarele reguli membranare:

[n in m]n[m]m→[n in∗m in∗m]n[m]m– daca avem configuratia care ne permite introducerea membranei n in membrana m, doua noi obiecte in∗m si in∗m sunt create in locul obiectului inm pentru a ajuta la realizarea acestei transformari;
in∗m[in m]in m→[in m d]in m – in prezenta obiectului in∗m, membrana in m este dizolvata;
[n in∗m]n[m]m →[m[n ]n]m – daca membrana elementara n contine obiectul in∗m, atunci membrana n este introdusa in membrana m;
[m[nout m ]n]m →[m[nout∗m out∗m]n]m – daca avem configuratia care ne permite extragerea membranei n din membrana m, doua noi obiecte out∗m si out∗m sunt create in locul obiectului outm pentru a ajuta la realizarea acestei extrageri;
out∗m[out m]aut m →[out md]aut m – in prezenta obiectului out∗m, membrana out m este dizolvata;
[m[n out∗m]n]m →[n ]n [m]m – daca membrana elementara n contine obiectul out∗m, atunci membrana n este extrasa din membrana m;
[m]mopen m →[md] mopen∗m – daca avem configuratia care ne permite dizolvarea membranei m, atunci aceasta este dizolvata si un nou obiect open∗m este creat in locul obiectului open m pentru a ajuta la dizolvarea membranei corespunzatoare open m;
open∗m[open m]open m → [open md]open m – in prezenta obiectului open∗m, membrana open m este dizolvata;
[n in∗m[t ]t]n →[n in∗m[t in∗m out∗n in∗n]t]n – daca membrana n contine alta membrana impreuna cu obiectul in∗m, atunci acest obiect este copiat in membrana interioara unde mai sunt create doua noi obiecte out∗n si in∗n care vor ajuta la obtinerea aceleasi configuratii pentru membrana n dupa ce toate obiectele marcate cu * au fost consumate;
[n out∗m[t ]t]n →[n out∗m[t out∗m out∗n in∗n]t]n– daca membrana n contine alta membrana si obiectul out∗m, atunci acest obiect este copiat in membrana interioara unde mai sunt create doua noi obiecte out∗n si in∗n care vor ajuta la obtinerea aceleasi configuratii pentru membrana n dupa ce toate obiectele marcate cu * au fost consumate.

Trebuie impuse anumite constrangeri in aplicarea regulilor de mai sus pentru a obtine o succesiune corecta de pasi:

Propozitia 1. Daca A si B sunt doi ambienti mobili, iar P este un sistem membranar astfel incat A ⇒aB si A |-P, atunci exista o succesiune de tranzitii

unde r1…ri sunt reguli membranare, Q este un sistem membranar care nu contine nici un obiect marcat cu * si B ⊢ Q..

Propozitia 2. Fie P si Q doua sisteme mebranare ce nu contin obiecte marcate cu * si A un ambient mobil astfel incat A |-P. Daca avem o succesiune de tranzitii

, atunci exista un ambient mobil B astfel incat B |- Q.. Daca un singur obiect marcat cu * este consumat, atunci avem A ⇒aB.

Daca avem doua sisteme mebranare P si Q care nu contin obiecte marcate cu * spunem ca P ⇒pQ daca avem o succesiune de tranzitii

, in care un singur obiect nemarcat cu stea este consumat.

Propozitia 3. |- este o bisimilaritate relativ la relatiile ⇒a şi ⇒p intre ambientii mobili si P sistemele corespunzatoare obtinute prin translatare, adica:

Pentru exemplificare se descrie pe larg protocolul taxiului prezentat in [16] utilizand ambientii mobili. Acest protocol este translatat in P sisteme si este urmarita evolutia lui prin aplicarea regulilor definite anterior.

2) Definirea unei semantici operationale a P sistemelor si traducerea acesteia intr-un sistem de rescriere

In [L31] am definit un cadru de lucru bazat pe „rewriting logic” pentru implementarea si investigarea proprietatilor sistemelor mebranare. In mare am urmat linia din J. Meseguer, G. Rosu, Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools, IJCAR'04: am definit o parte ecuationala pentru specificarea configuratiilor si am utilizat regulile de rescriere pentru a descrie semantica operationala. In articolul lui Meseguer si Rosu se utilizeaza o semantica bazata pe ceea ce urmeaza a fi calculat (CPS - Continuation Passing Style). Aceasta semantica este potrivita in general limbajelor de programare unde sunt prezente structuri de control. Partea de control a sistemelor membranare este foarte simpla si diferita de cea a limbajelor de programare. Ea consta din aplicarea regulilor de evolutie intr-o maniera maximal-paralela in acord cu prioritatile lor. Definirea de semantici pentru P sisteme in logica de rescriere a relevat un aspect interesant: evolutia interna, comunicarea si dizolvarea in interiorul unei membrane complexe se pot intercala. Aceasta conduce la o un SOS local asincron pentru P sisteme.

In timpul vizitei la University of Illinois at Urbana-Champaign (UIUC) au fost prezentate principalele provocari pe care sistemele membranare le pun in fata motoarelor de rescriere. De notat ca principalele discutii de la la UIUC au avut loc cu Prof. Jose Meseguer, creatorul paradigmei "rewriting logic" si a sistemului Maude bazat pe rewriting logic, si Prof. Grigore Rosu, autorul metodei de demonstrare prin coinductie circulara. Aceste provocari sunt impartite pe doua nivele. Pe primul nivel se gasesc implementarile principalelor mecanisme de control din sistemele membranare: rescriere maximala paralalela simpla sau in prezenta prioritatilor, promotorilor si a inhibitorilor. S-au discutat modalitatile in care acestea pot fi implementate eficient utilizand motoarele de rescriere, in special cel din Maude. Deoarece Maude este bazat pe logica rescrierii care este reflectiva, s-a ajuns la concluzia ca acesta poate suporta toate mecanismele de control din sistemele membranare. Totusi, in lipsa unor facilitati de implementare a strategiilor de rescriere specifice, face ca aceasta descriere sa fie anevoioasa si greu de utilizat. S-a evidentiat necesitatea creerii unui cadru de lucru specific pentru sistemele membranare. La al doilea nivel se gaseste aplicarea instrumentele de analiza si verificare existente pentru investigarea proprietatilor sistemelor membranare. Model-checkerul din Maude a fost deja utilizat pe implementarea initiala a P sistemelor in Maude. In perioada vizitei, am contribuit la dezvoltarea unui demonstrator bazat pe coinductie circulara. Acest demonstrator se gaseste in faza de prototip acum si urmeaza a fi facut public in curand. O provocare interesanta si dificila este cea de utilizare a demonstratorului pentru gasirea/dovedirea de relatii bismilaritate intre P sisteme.

Articolele [L5] si [L19] se inscriu in linia de cercetare descrisa in partea introductiva relativ la investigarea proprietatilor algebrice si coalgebrice a P sistemelor. In [L5] sunt cercetate proprietatile (co)algebrice ale automatelor multiset de tip Mealy (MmA). Aceste MmA alcatuiesc componentele paralele ale automatelor membranare simple de tip Mealy (sMMA), care au fost introduse in cadrul celui de al doilea articol. Aceste sMMA constitue o prima tentativa in reprezentarea – simularea sistemelor membranare cu ajutorul masinilor teoretice, pentru care se pot studia notiuni si proprietati de tipul comportamentului, bisimilaritate etc.

Atat obiectele dintr-o membrana cat si membranele dintr-o membrana parinte pot fi privite ca multiseturi, adica functii definite pe multimea obiectelor, respectiv a membranelor, cu valori in multimea numerelor naturale. Imaginea unui obiect printr-un multiset reprezinta numarul de instante a obiectului respectiv. Tinand seama ca acest numar este un cardinal, notiunea de multiset poate fi extinsa la functii cu valori in multimea numerelor cardinale. Operatiile definite pe multimea cardinalilor, adunare, inmultire si ridicare la putere, pot fi translatate atunci pe multimea multiseturilor. De asemenea, relatia de ordine a cardinalilor ne permite introducerea unei relatii de ordine partiale pe multimea multiseturilor, compatibila cu operatiile. Intrucat ordinea cardinalilor este totala, putem defini minimul si maximul a doua multiseturi, operatii compatibile cu adunarea si inmultirea multiseturilor. Daca alegem, de exemplu, operatia de inmultire, suntem condusi la o structura algebrica dubla, de semigrup si de latice, compatibile, asa incat este indeplinita relatia de separatie

. Ordinea laticeala coincide cu cea definita. O astfel de structura a fost denumita algebra a resurselor (si respectiv apartness-lattice order semigroup). In primul rand a fost realizat un studiu al proprietatilor algebrice ale acestor structuri. Relatia de ordine laticeala ne permite apoi sa definim o qvasi-uniformitate pe algebra resurselor, fata de care operatiile (laticeale si de semigrup) sunt uniform-continue. Dar topologia obtinuta pe aceasta cale este destul de saraca in proprietati, iar mijloacele de masura furnizate sunt doar pseudo-qvasi-metrici. Din acest motiv, a fost introdusa si studiata notiunea de (pseudo-)supermetrica. Multimea acestora este izomorfa cu conul functiilor reale aditive si crescatoare, definite pe algebra resurselor (multime numita dualul acesteia). Au fost investigate o serie de conditii de completitudine si relatiile dintre ele (completitudine conditionala,

-completitudinea, completitudine metrica, conditia Cantor, continuitatea Scott, etc). Aceste legaturi sunt utile pentru a stabili conditii suficiente de punct fix. Evolutia unei structuri celulare poate fi definita printr-un operator de evolutie, care la fiecare pas transforma celula intr-o alta celula. Stationarea procesului coincide cu obtinerea unui punct fix pentru acest operator. Studiul descris pe scurt mai sus a fost concretizat in rezultatele publicate sau trimise spre publicare [L8] si [L27].

Activitatile prevazute in plan au fost indeplinite in proportie cu gradul de suprapunere a perioadei de desfasurare fata de perioada raportata, dupa cum urmeaza:

[1] O. Andrei, G. Ciobanu, D. Lucanu. Structural Operational Semantics of P Systems. Proceedings WMC6, LNCS vol.3850, Springer, 32-49, 2006.

[2] O. Andrei, G. Ciobanu, D. Lucanu. Executable Specifications of the P Systems. In Membrane Computing. WMC5, Lecture Notes in Computer Science vol.3365, Springer, 127-146, 2005.

[3] L. Cardelli, A. Gordon. Mobile Ambients, Proc. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science vol. 1378, Springer, 140-155, 1998.

[4] G. Ciobanu. Distributed Algorithms over Communicating Membrane Systems. Biosystems vol.70, Elsevier, 123-133, 2003.

[5] G. Ciobanu, V.A. Zakharov Encoding Mobile Ambients into the p-calculus. Proc. Perspectives of System Informatics, Lecture Notes in Computer Science, Springer, 2006.

[6] G. Ciobanu, M. Gontineac. Mealy membrane automata and P systems complexity. In M.A.Gutierrez-Naranjo, Gh.Paun, M.J.Perez-Jimenez (Eds.): Cellular Computing; complexity aspects}, ESF Workshop, Fenix Editora, Sevilla, 149-164, 2005.

[7] M. Clavel, F. Durán, S. Eker, P. Lincoln, N.~Marti-Oliet, J. Meseguer, J.F. Quesada.
Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science, vol.285, 187-243, 2002.

[8] Giavitto L., Michael O., The Topological Structures of Membrane Computing, Fundamenta Informaticae, vol. 49 , 123 – 145, 2002.

[9] D. Hirschkoff, D. Teller, P. Zimmer. Using Ambients to Control Resources Proc. CONCUR’02, Lecture Notes in Computer Science vol.2421, Springer, 288-303, 2002.

[10] G. Kahn. Natural semantics, Technical Report 601, INRIA Sophia Antipolis, 1987

[11] S.N. Krishna. On the Efficiency of a Variant of P Systems with Mobile Membranes Cellular Computing; complexity aspects, ESF PESC Exploratory Workshop, Fenix Editora, Sevilla, 237-246, 2005.

[13] R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol.B, 1201-1242, Elsevier Science, 1990.

[14] P. Mosses. Modular Structural Operational Semantics. BRICS RS 05-7, 2005.

[15] Gh. Paun. Computing with membranes; An introduction, Bulletin of EATCS, vol. 68, 139-152, 1999.

[17] Paun G., Rozenberg G., Salomaa A., Membrane Computing with External Output, Fundamenta Informaticae, 41(3), 259-366, 2000.

[18] Paun G., P Systems with active Membranes: Attacking NP Complete Problems, J. Automata, Languages, and Combinatorics 2000.

[19] Paun G., Dassow J., On the Power of Membraning Computing, J. of Universal Computer Science, 5(2), 33-49, 1999.

[20] A. Pitts. Semantics of programming languages. Lecture Notes, University of Cambridge, 1989.

[21] G. Plotkin. Structural operational semantics. Journal of Logic and Algebraic Programming vol.60, 17-139, 2004.

[22] Stadler B.M.R., Stadler P.F., The Topology of Evolutionary Biology, in G.Ciobanu, G. Rozenberg (Eds.): Modeling in Molecular Biology, Springer Verlag, Natural Computing Series 267-286, 2005.

[23] Stadler B.M.R., Stadler P.F., Wagner P., Fontana W., The topology of the possible: Formal spaces underlying patterns of evolutionary change, .Theor.Biol. vol.213, 241-274, 2001.

[24] Stadler B.M.R., Stadler P.F., Molecular Replicator Dynamics, Adv. Complex Systems vol.6, 47-77, 2003.

[25] E. Visser. A Survey of Strategies in Rule-Based Program Transformation Systems. Journal of Symbolic Computation vol.40, 831-873, 2005.

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

<<

Parteneri participanti

Termen
planificat/realizat

Planificat

Realizat

Abatere

Planificat

Realizat

Abatere

Planificat

Realizat

Abatere

Lucrari IEEE sau ACM:

Lucrari in alte publicatii nationale/internationale

Rapoarte tehnice

Thesis

Books

<<

Parteneri participanti

Termen planificat/realizat

Planificat

Realizat

Abatere

Planificat

Realizat

Abatere

Planificat

Realizat

Abatere

Lucrari IEEE sau ACM:

Lucrari in alte publicatii nationale/internationale

Rapoarte tehnice

Thesis

Books

Termen
planificat/realizat