Automaty nieskończone 1000-2M22AN
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.
Kierunek podstawowy MISMaP
Rodzaj przedmiotu
Wymagania (lista przedmiotów)
Założenia (lista przedmiotów)
Koordynatorzy przedmiotu
W cyklu 2025Z: | W cyklu 2024Z: |
Efekty kształcenia
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
Kryteria oceniania
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.
Literatura
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.
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: