témavezető: Ésik Zoltán
helyszín (magyar oldal): SZTE TTIK Matematika- és Számítástudományok Doktori Iskola 6720 Szeged, Aradi vértanúk tere 1. helyszín rövidítés: MatDI
A kutatási téma leírása:
A számítástudományban a rekurziót általában függvények, funkcionálok, funktorok fixpontjaiként tárgyalják. Korábbi vizsgálatok [5,6] kimutatták, hogy az iterációs Lawvere elméletek azonosságai az azonosságok teljes leírását adják lényegében minden fixpont modellben.
Az egyik cél annak vizsgálata, hogy a modellek egyéb (járulékos) struktúrája hogyan viszonyul az alapstruktúrához. Mely modellekben igaz az, hogy a járulékos struktúra azonosságai végesen axiomatizálhatóak az iterációs elméletek azonosságai felett? A vizsgálatok egy széles keretét az ún. processzus algebrák szolgáltatják, ld. [2,3]. Ezek olyan fixpont modellek, amelyekben egy additív struktúra is értelmezett, és esetleg jelen vannak más műveletek és konstansok is. Az irodalomban számos processzus algebra ismert, amelyek a processzusok különböző szemantikus ekvivalenciájaihoz tartoznak, ld. [10]. A [4] cikkben bebizonyítottuk, hogy a biszumulációs ekvivalencia relációhoz tartozó processzus algebrák azonosságai végesen axiomatizálhatóak az iterációs elméletek azonosságai felett. Azt várjuk, hogy hasonló véges axiomatizálási eredményeket érvényesek más szemantikus ekvivalenciákra nézve is. Ezt felhasználva azt is várjuk, hogy a tekintett azonosságok végesen axiomatizálhatók kvázi-azonosságok segítségével. Ezek az eredmények nagy előrelépést jelentenének az eddig elért eredményekhez képest. Pld. a [2] könyvben szereplő teljes axiomatizálások mindegyike végtelen formulákat is tartalmaz.
A számítástudomány sok tekintetben leíró tudomány. A vizsgálatok egy jó része arra vonatkozik, hogyan lehet egy hardware, software vagy egyéb rendszert leírni (specifikálni), és hogyan lehet az egyik leírásról áttérni egy másikra. A processzus algebrák azonosságainak vizsgálata annak jobb megértést szolgálja, hogy hogyan lehet konkurens folyamatok leírásain ekvivalens átalakításokat végezni.
Másik célkitűzés az, hogy az iterációs elméletek kalkulusának segítségével axiomatikus alapokra helyezzük az automaták és formális nyelvek elméletét. Az utóbbi években sikerült megmutatni, hogy a formális nyelvek elméletének számos alapvető eredménye csak a fixpont művelet néhány egyszerű azonosságán múlik. Ilyen eredmények Kleene nevezetes tétele a reguláris nyelvekre [7], racionális hatványsorokra [8], Parikh alapvető tétele a környezetfüggetlen nyelvekre [1,11] , valamint Greibach Normal Forma Tétele [9]. A fixpontok általános elméletét felhasználásával várhatóan sor kerülhet további klasszikus eredmények, és néhány új eredmény olyan bizonyításának megadására, melyben csak a fixpont művelet azonosságait használjuk.
[1] L. Aceto, Z. Ésik, A. Ingolfsdottir: A fully equational proof of Parikh's theorem,
Theoretical Informatics and Applications, 36(2002), 129--154
[2] J. C. Baeten and W. P. Weijland: Process algebra. Cambridge Tracts in Theoretical Computer Science, 18. Cambridge University Press, Cambridge, 1990.
[3] J. A. Bergstra et al., eds.: Handbook of Process Algebra, Elsevier, 2001.
[4] S. L. Bloom, Z. ésik, D. Taubner: Iteration theories of synchronization trees,
Information and Computation, 102(1993), 1-55.
[5] S. L. Bloom, Z. Ésik: Iteration Theories: The Equational Logic of Iterative Processes,
EATCS Monograph Series on Theoretical Computer Science, XVI+630 pages, Springer-Verlag, 1993.
[6] S. L. Bloom and Z. Ésik: The equational logic of fixed points, Theoretical Computer Science, 179(1997), 1--60.
[7] Z. Ésik, W. Kuich, Equational Axioms for a Theory of Automata, in: Formal Languages and Applications, Springer, 2004, 183--196.
[8] Z. Ésik, W. Kuich: Inductive *-semirings, Theoret. Comput. Sci, 324(2004), 3--33.
[9] Z. Ésik, H. Leiss: Algebraically complete semirings and Greibach normal form,
Annals of Pure and Applied Logic, 103(2005), 173--203.
[10] R. van Glabbeek: The linear time - branching time spectrum, in:Handbook of Process Algebra, North-Holland Publishing Co., Amsterdam, 2001,
[11] M. W. Hopkins, D. Kozen: Parikh's Theorem in Commutative Kleene Algebra. LICS 1999, IEEE Computer Soc. Press, 1999, 394-401.
felvehető hallgatók száma: 1
Jelentkezési határidő: 2012-07-31
2024. IV. 17. ODT ülés Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).
Bejelentkezés
