Automaty nieskończone

informatyka

monograficzne

Języki, automaty i obliczenia 1000-214bJAO

Złożoność obliczeniowa 1000-218bZO

Algorytmiczna analiza automatów o nieskończenie wielu stanach: automaty ze stosem, automaty z licznikami, sieci Petriego.

Nieskończoność przestrzeni stanów jest wszechobecna w informatyce 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 nieskończony, niż

sztucznie go ograniczać do zbioru skończonego ale astronomicznie wielkiego. Tak

jest m.in. w przypadku automatów ze stosem (PDA) czy VASS, które są

równoważne siecią Petriego. Mimo nieskończonej przestrzeni stanów, istnieją tu

algorytmy rozstrzygające istotne problemy decyzyjne, takie jak niepustość języka,

inkluzje języków, osiągalność albo pokrywalność. Przyjrzymy się najciekawszym

problemom w tej dziedzinie, w szczególności rozstrzygalności osiągalności w

sieciach Petriego.

Opowiemy o tematach wybranych spośród:

1) Automaty ze stosem (np. niepustość języka);

2) Podstawowe systemy o nieskończonej liczbie stanów, dla których

osiągalność jest nierozstrzygalna (automat z dwoma stosami, automaty

licznikowe);

3) Zbiory semiliniowe, ich własności i zastosowania. Arytmetyka Presburgera;

4) Twierdzenie Parikha i jego zastosowania (np. unarne automaty ze stosem

rozpoznają języki regularne);

5) Techniki oparte o WQO (rozstrzygalność uniwersalności VASS);

6) Programowanie liniowe i jego zastosowania (osiągalność binarnych 1-VASS

jest w NP);

7) Pokrywalność i ograniczoność w VASS (w tym technika Rackoffa);

8) Ciekawe przykłady VASS (w tym o niesemiliniowym zbiorze osiągalności);

9) Szybko rosnąca hierarchia i Ackermann-trudność osiągalności w VASS;

10) Osiągalność w VASS jest rozstrzygalna.

R. Lipton: The Reachability Problem Requires Exponential Space. University of Yale Research Report (63), 1976.

C. Rackoff: The Covering and Boundedness Problems for Vector Addition Systems, Theoretical Computer Science 1978.

J. Hopcroft, J. Pansiot: On the Reachability Problem for 5-Dimensional Vector Addition Systems, Theoretical Computer Science 1979.

F. Eisenbrand, G. Shmonin: Carathéodory bounds for integer cones, Operations Research Letters 2006.

C. Haase, S. Kreutzer, J. Ouaknine, J. Worrell: Reachability in Succinct and

Parametric One-Counter Automata, CONCUR 2009.

S. Schmitz: The complexity of reachability in vector addition systems, ACM SIGLOG News 2016.

C. Haase: A Survival Guide to Presburger Arithmetic, ACM SIGLOG News 2018.

J. Leroux, S. Schmitz: Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension, LICS 2019.

S. Lasota: VASS reachability in three steps, 2020.

W. Czerwiński, Ł. Orlikowski: Reachability in Vector Addition Systems is Ackermann-complete, FOCS 2021.

Wiedza

Student pogłębia wiedzę o klasycznych zastosowaniach teorii automatów.

Umiejętności

Student umie rozpoznać granice obliczalności różnych wariantów modeli.

Student potrafi modelować różne problemy za pomocą odpowiednich automatów.

Kompetencje

Student rozumie narzędzia matematyczne wypracowane we współczesnej teorii

automatów i potrafi z nich korzystać zarówno w samej informatyce, jak i w jej

zastosowaniach

Zadania gwiazdkowe i egzamin ustny.

W przypadku zaliczania przedmiotu przez doktoranta, dodatkowym elementem

zaliczenia będzie rozwiązanie przynajmniej jednego zadania z gwiazdką bądź

zapoznanie się z oryginalnym, będącym blisko aktualnego frontu badań, artykułem

naukowym i rozmowa z wykładowcą na temat tego artykułu.