wykład

ćwiczenia

USOS

Ogłoszenia:

• Ćwiczenia zostały przesunięte na godz. 12:00, czyli o 15 minut wcześniej.

Egzamin:

• środa 13 czerwca, godz. 10-13, s. 5730 albo 5870
• zadania
• zapisy na egzamin ustny

Wykłady:

• wykład 1: wprowadzenie, motywacje, osiągalność dla grafów automatów ze stosem
• wykład 2: stratne maszyny licznikowe, wprowadzenie do automatow czasowych
• wykład 3: problem pustości dla automatów czasowych -- automat regionowy
• wykład 4: problemy nierozstrzygalne: uniwersalność, determinizowalność, itp.
• wykład 5: automaty czasowe z 1 zegarem a stratne modele obliczeń
• wykład 6: sieci Petriego: definicje, dolna granica EXPSPACE
• wykład 7: dolna granica EXPSPACE c.d., algorytm w EXPSPACE dla problemu pokrywalności
• wykład 8: dowód rozstrzygalności osiągalności (część I): relacja osiągalności jest prawie semi-liniowa
• wykład 9: dowód rozstrzygalności osiągalności (część II): relacja osiągalności pomiędzy zbiorami semi-liniowymi jest prawie semi-liniowa
• wykład 10: dowód rozstrzygalności osiągalności (część III): semi-liniowy separator
• wykład 11: równoważność bisymulacyjna, dowód nierozstrzygalności dla sieci Petriego
• wykład 12: baza bisymulacyjna, równoważność bisymulacyjna z przejściami epsilonowymi, PDA, problem rownoważności DPDA a bisymulacja
• wykład 13: dowód rozsztrzygalności równoważności DPDA (część I): gramatyki 1go rzędu, gra Refuter-Prover
• wykład 14: dowód rozsztrzygalności równoważności DPDA (część II): Prover ma (n,g)-strategię
• wykład 15: dowód rozsztrzygalności równoważności DPDA (część III): Prover ma strategię finitarną

Zadania:

• zadanie 1 (wqo)
• zadanie 2 (automaty czasowe)
• zadanie 3 (sieci Petriego)
• zadanie 4 (sieci Petriego) + zadanie z gwiazdką
• zadanie 5 (bisymulacja) + zadanie 6 (wyrażalność językowa)

Ćwiczenia:

• ćw. 1: wqo
• ćw. 2: wqo c.d., dowód rozstrzygalności osiągalności dla stratnych maszyn licznikowych, warianty automatów czasowych
• ćw. 3: wqo c.d., warianty automatów czasowych c.d.
• ćw. 4: warianty automatów czasowych c.d., zastosowania wqo
• ćw. 5: zastosowania wqo c.d., sieci Petriego, stratne modele obliczeń
• ćw. 6: sieci Petriego, zbiory semiliniowe
• ćw. 7: głównie rozstrzygalność różnych problemów dla sieci Petriego
• ćw. 8: zbiory semiliniowe, logika Presburgera
• ćw. 9: zbiory semiliniowe, logika Presburgera
• ćw. 10: ćwiczenia z dowodu rozstrzygalności Leroux
• ćw. 11: relacja bisymulacji
• ćw. 12: relacja bisymulacji c.d.
• ćw. 13: relacja bisymulacji c.d., wyrażalność różnych wariantów automatów ze stosem
• ćw. 14: słaba bisymulacja, relacja bisymulacji c.d.

Literatura:

• R. Alur, D. L. Dill, A theory of timed automata
• R. Alur, M. Parthasarathy, Decision problems for timed automata: a survey
• O. Finkel, On decision problem for timed automata
• J. Ouaknine, J. Worrell, On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap
• S. Lasota, I. Walukiewicz, Alternating timed automata
• J. Esparza, Decidability and complexity of Petri net problems — an introduction
• C. Rackoff, The covering and boundedness problems for vector addition systems
• J. Leroux, The general vector addition system reachability problem by Presburger inductive invariants
• J. Leroux, Vector Addition System Reachability Problem: A Short Self-Contained Proof
• P. Jancar, Decidability of DPDA Language Equivalence via First-Order Grammars

Zaliczenie:

• aby zaliczyć przedmiot należy uzyskać jedną trzecią punktów z zadań oraz zdać egzamin
• punkty uzyskane z zadań będą stanowić jedną trzecią oceny końcowej, a ocena z egzaminu dwie trzecie