Systemy nieskończone

monograficzne

Nieskończoność przestrzeni stanów jest wszechobecna w informatyce (przynajmniej tej teoretycznej), prowadzi do niej np. nieograniczona głębokość stosu czy nieograniczona współbieżność. Często lepiej rozważać zbiór stanów, który jest niekończony, niż sztucznie go ograniczać do zbioru skończonego ale astronomicznie wielkiego. Tak jest w m.in. przypadku automatów rejestrowych, automatów czasowych, sieci Petriego, czy grafów bezkontekstowych. Mimo nieskończonej przestrzeni stanów, istnieją tu algorytmy rozstrzygające istotne problemy decyzyjne, takie jak osiągalność albo równoważność. Przyjrzymy się najciekawszym problemom w tej dziedzinie. W szczególności zaprezentuję w całości dwa trudne dowody: rozstrzygalności osiągalności w sieciach Petriego i równoważności deterministycznych automatów ze stosem.

Program:

1. Wprowadzenie: modele o nieskończenie wielu stanach, problemy decyzyjne, motywacja - zastosowania w modelowaniu i weryfikacji programów, granice rozstrzygalności (1 wykład)

2. Automaty czasowe (lub automaty rejestrowe) i ich analiza symboliczna(2 wykłady)

3. FIFO-automaty i automaty licznikowe z błędami (1 wykład)

4. Sieci Petriego, przemienne grafy bezkontekstowe (2 wykłady)

5. Równoważność bisymulacyjna (2 wykłady)

6. Rozstrzygalność problemów decyzyjnych dla automatów czasowych z 1 zegarem i automatów rejestrowych z 1 rejestrem (1 wykłady)

7. Rozstrzygalność problemu równoważności deterministycznych automatów ze stosem (3 wykłady)

8. Rozstrzygalność problemu osiągalności dla sieci Petriego (3 wykłady)

Świeża literatura naukowa. W szczególności:

1. Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, ed., Handbook of Process Algebra, Elsevier, 2001.

2. Jerome Leroux, Demystifying reachability in Vector Addition Systems, LICS 2015.

3. Petr Jancar, Bisimulation Equivalence of 1st Order Grammars, ICALP 2014.

4. Roadmap of infinite results, http://www.brics.dk/~srba/roadmap/roadmap.pdf

5. S. Lasota, I. Walukiewicz, Alternating Timed Automata. ACM Transactions on Computational Logic 9(2), 2008.

6. P. Schnoebelen, Lossy Counter Machines Decidability Cheat Sheet. RP'10, LNCS 6227, 2010.

Umiejętności

1. Potrafi formalizować opis systemu współbieżnego w wybranym modelu (K_U02, K_U06).

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

Wiedza

1. Ma uporządkowaną, podbudowaną teoretycznie wiedzę ogólną w zakresie algorytmów i złożoności dotyczących analizy modeli nieskończenie stanowych (K_W02)

2. Ma ogólną wiedzę w zakresie modeli systemów współbieżnych i ich wzajemnej relacji (K_W02, K_W04, K_W05).

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

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

Umiejętności

1. Potrafi formalizować opis systemu w wybranym modelu (K_U02, K_U06).

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

3. Potrafi pozyskiwać informacje z literatury, Internetu oraz innych wiarygodnych źródeł, integrować je, dokonywać ich interpretacji (K_U02)

Kompetencje

1. Zna ograniczenia własnej wiedzy i rozumie potrzebę dalszego kształcenia (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).

Albo zaliczenie pisemne (przygotowanie notatek z któregoś z wykładów) albo ustne (rozmowa na temat wskazanego artykułu naukowego).