Problemy decyzyjne dla systemów nieskończonych

Informacje ogólne

Kod przedmiotu:	1000-2M11PDG
Kod Erasmus / ISCED:	11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
Nazwa przedmiotu:	Problemy decyzyjne dla systemów nieskończonych
Jednostka:	Wydział Matematyki, Informatyki i Mechaniki
Grupy:	Przedmioty obieralne dla informatyki Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka
Strona przedmiotu:	http://www.mimuw.edu.pl/~sl/teaching/PDSN
Punkty ECTS i inne:	(brak) Podstawowe informacje o zasadach przyporządkowania punktów ECTS: roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS; tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h; 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się; tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS; nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta. zobacz reguły punktacji
Język prowadzenia:	angielski
Rodzaj przedmiotu:	monograficzne
Skrócony opis:	Przegląd wybranych modeli obliczeń, takich jak: automaty rejestrowe, sieci Petriego czy grafy bezkontekstowe, dla których, mimo nieskończonej przestrzeni stanów, istnieją algorytmy rozstrzygające istotne problemy decyzyjne, takie jak osiągalność albo równoważność. 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.
Pełny opis:	1. Wprowadzenie: modele o nieskończenie wielu stanach, problemy decyzyjne, motywacja - zastosowania w weryfikacji programów, granice rozstrzygalności (1 wykład) 2. Automaty czasowe (1 wykład) 3. Automaty na słowach z danymi: automaty rejestrowe, automaty danowe (2 wykłady) 4. FIFO-automaty i automaty licznikowe z błędami (2 wykłady) 5. Sieci Petriego, przemienne grafy bezkontekstowe (2 wykłady) 6. Równoważność bisymulacyjna (1 wykład) 7. Rozstrzygalność problemów decyzyjnych dla automatów czasowych z 1 zegarem i automatów rejestrowych z 1 rejestrem (2 wykłady) 8. Rozstrzygalność problemu równoważności deterministycznych automatów ze stosem (2 wykłady) 9. Rozstrzygalność osiągalności dla sieci Petriego (2 wykłady)
Literatura:	Ś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, Vector Addition System Reachability Problem (A Short Self-Contained Proof), praca zgłoszona do publikacji. 3. Petr Jancar, Short Decidability Proofs for DPDA Equivalence and 1st Order Grammar Bisimilarity, praca zgłoszona do publikacji. 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), Article 10, 2008. 6. P. Schnoebelen, Lossy Counter Machines Decidability Cheat Sheet. RP'10, LNCS 6227, 2010.
Metody i kryteria oceniania:	Albo zaliczenie pisemne (przygotowanie nontatek z któregoś z wykładów) albo ustne (roznowaz na temat wskazanego artykułu naukowego).

Przedmiot nie jest oferowany w żadnym z aktualnych cykli dydaktycznych.

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.