Ogłoszenia:

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

Egzamin:

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:

Ć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:

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