Teoria współbieżności

informatyka

obowiązkowe

w sali

Tworzenie systemów współbieżnych jest trudną sztuką, dlatego od zarania informatyki rozważa się różne modele matematyczne takich systemów.

Celem wykładu jest przybliżenie słuchaczom najważniejszych i najciekawszych z nich:, m.in. sieci Petriego i algebry procesów.

Dużo uwagi poświęcamy zagadnieniu automatycznej analizy modeli systemów współbieżnych, w szczególności złożoności obliczeniowej tego zagadnienia.

Część ćwiczeń odbywa się w laboratorium i poświęcona jest pracy z wybranymi narzędziami do modelowania i analizy systemów współbieżnych.

Tworzenie systemów współbieżnych jest trudną sztuką, dlatego od zarania informatyki rozważa się różne modele matematyczne takich systemów. Celem wykładu jest przybliżenie słuchaczom najważniejszych i najciekawszych z nich:, m.in. sieci Petriego i algebry procesów. Dużo uwagi poświęcamy zagadnieniu automatycznej analizy modeli systemów współbieżnych, w szczególności złożoności obliczeniowej tego zagadnienia. Część ćwiczeń odbywa się w laboratorium i poświęcona jest pracy z wybranymi narzędziami do modelowania i analizy systemów współbieżnych.

Program:

I. Wstęp

1. Motywacje, klasyfikacja modeli, narzędzia; przeplotowe i nieprzeplotowe modele systemów współbieżnych.

2. Czas liniowy a czas rozgałęziony: własności temporalne (LTL, CTL).

II. Sieci Petriego

3. Sieci Petriego: interakcja współbieżności, zależności i konfliktu.

4. Teoria śladów i jej związki z sieciami Petriego; wzmianka nt automatów asynchronicznych.

III. Algebry procesów

5. CCS: współbieżność i komunikacja; wzmianka na temat innych algebr procesów.

6. Bisymulacja jako semantyczna równoważność procesów.

IV. Analiza systemów wspólbieżnych

7. Rozstrzygalność problemu osiągalności dla sieci Petriego.

8. Problem równoważności bisymulacyjnej: nierozstrzygalność, złożoność obliczeniowa w szczególnych przypadkach.

Bergstra, J., Ponse, A., Smolka, S., ed. Handbook of Process Algebra, Elsevier, 2001

R. Milner, Communication and Concurrency, Prentice Hall 1995

W. Reisig, Sieci Petriego, Wydawnictwa Naukowo Techniczne 1988

W. Reisig, G. Rozenberg (ed), Lectures on Petri Nets I: Basic Models, Springer 1998

J. Esparza, M. Nielsen, Decidability Issues for Petri Nets - a survey, Bulletin of the EATCS 52:244-262 (1994)

C. Rackoff, The covering and boundedness problems for vector addition systems, Theoretical Computer Science:6(2), 1978

V. Sassone, M. Nielsen, G. Winskel, Models for Concurrency: Towards a Classification, Theoretical Computer Science:170(1–2), 1996

V. Diekert, G. Rozenberg (ed), The Book of Traces, World Scientific 1995

S. Rao Kosaraju, Decidability of Reachability in Vector Addition Systems (Preliminary Version), STOC 1982

J. Leroux, Vector Addition Systems Reachability Problem (A Simpler Solution), Turing-100 2012

Wiedza

1. Zna techniki synchronizacji procesów i komunikacji międzyprocesowej w scentralizowanym i rozproszonym modelu programu współbieżnego [K_W02].

2. Zna algorytmy wzajemnego wykluczania i uzgadniania w systemach rozproszonych [K_W05].

3. Ma ogólną wiedzę w zakresie modeli systemów współbieżnych i ich wzajemnej relacji.

4. Ma usystematyzowaną wiedzę w zakresie zjawisk zachodzących w systemach współbieżnych.

5. Rozumie korzyści płynące z formalnego modelowania zagadnień współbieżności oraz ograniczenia modeli formalnych.

6. Ma podstawową wiedzę w zakresie złożoności obliczeniowej podstawowych problemów weryfikacyjnych.

Umiejętności

1. Potrafi zastosować mechanizmy synchronizacji procesów i wątków w wybranych technologiach w zależności od architektury i możliwości konkretnego komputera [K_U06].

2. Posługuje się nowoczesnymi technologiami rozpraszania i zrównoleglania obliczeń [K_U08].

3. Ma umiejętności językowe w zakresie informatyki zgodne z wymaganiami określonymi dla poziomu B2+ Europejskiego Systemu Opisu Kształcenia Językowego, w szczególności: identyfikuje główne i poboczne tematy wykładów, pogadanek, debat akademickich, dyskusji, czyta ze zrozumieniem i krytycznie analizuje teksty akademickie, zabiera głos w dyskusji lub debacie naukowej, streszcza ustnie informacje, wyniki badań, opinie i argumenty autora zawarte w tekście naukowym [K_U14].

4. Potrafi formalizować opis systemu współbieżnego w wybranym modelu.

5. Potrafi opisać wybrane zagadnienia współbieżności w sposób zrozumiały dla niespecjalisty.

6. Potrafi formalizować zadane proste własności w logice temporalnej.

Kompetencje

1. Zna ograniczenia własnej wiedzy i rozumie potrzebę dalszego kształcenia, w tym zdobywania wiedzy pozadziedzinowej [K_K01].

2. Potrafi precyzyjnie formułować pytania, służące pogłębieniu własnego zrozumienia danego tematu lub odnalezieniu brakujących elementów rozumowania [K_K02].

3. Potrafi pracować zespołowo, w tym w zespołach interdyscyplinarnych; rozumie konieczność systematycznej pracy nad wszelkimi projektami, które mają długofalowy charakter [K_K03].

4. Potrafi formułować opinie na temat podstawowych zagadnień informatycznych związanych ze współbieżnością [K_K06].

Egzamin ustny, 3 zagadnienia losowane z listy publikowanej na miesiąc przed egzaminem.