Wyklad monograficzny WZTPW

Wykład monograficzny Wybrane zagadnienia teorii procesów współbieżnych, semestr zimowy 2002/2003

Termin:
- wykład: poniedziałki, 10:15, sala 5830
- ćwiczenia: poniedziałki, 12:00, sala 5830
Opis wykładu
Egzaminy
- Egzamin pisemny: piątek 24 stycznia 2003, godz. 11:00, sala 3140
  - zadania z egzaminu
  Egzamin poprawkowy: środa 12 marca 2003, godz. 12:00, pokój 5730
- Zadania z egzaminu sprzed dwoch lat
Notatki do wykładu uaktualnione 24.01.2003: wykłady 1--8
- Wykład 1: Wprowadzenie, przykłady
- Wykład 2: Składnia i semantyka CCS
- Wykład 3: Prawa równościowe
- Wykład 4: Silna bisymulacja
- Wykład 5: Słaba bisymulacja
  - przykład 1: Zarządca
- Wykład 6: Równoważność obserwacyjna
  - przykład 2: Alternating Bit Protocol
- Wykład 7: Nierozstrzygalność rownoważności procesów
- Wykład 8: Bisymulacja, logika i gry
- Wykład 9: Narzędzia: CWB, CWB-NC
  - UWAGA: zajęcia 9 grudnia o 10:15 przy komputerach, w LABORATORIUM 6
- Wykład 10: Aksjomatyzacja i algorytm sprawdzania równoważności procesów skończeniestanowych
- Wykład 11: CCS z czasem, protokół BRP
- Wykład 12: Przykład weryfikacji: protokół MSMIE
Uwagi:
Literatura podstawowa:
- CCS:
  - R. Milner Communication and Concurrency, Prentice Hall, 1989.
  - R. Milner Operational and Algebraic Semantics of Concurrent Processes, rozdział 19 w Handbook of Theoretical Computer Science, ed. J. van Leuveen, Elsevier Science Publishers 1990.
- Bisymulacja z dokładnością do ... :
  - D. Sangiorgi, D. Milner Techniques of "weak bisimulation up to", Proc. CONCUR'92, LNCS 630, 1992.
  - S. Arun-Kumar, M. Hennessy An Efficiency Preorder for Processes, Acta Informatica, 29:737--760, 1992. plik .ps.gz
- Rozszerzenia CCS: TCCS, SCCS
  - Moller, F., Tofts, C. A Temporal Calculus of Communicating Systems, Proc. CONCUR'90, LNCS 458, strony 401-415, 1990.
  - Moller, F., Tofts, C. Relating Proceses with Respect to Speed, Proc. CONCUR'91, LNCS 527, 1991.
  - R. Milner Calculi for Synchrony and Asynchrony, Theoretical Computer Science 25, 1983, strony 267-310.
- Spektrum równoważności behawioralnych:
  - Bergstra, J., Ponse, A., Smolka, S., ed. Handbook of Process Algebra, Elsevier, 2001, rozdział 1.
- Weryfikacja: sprawdzanie wlasności, sprawdzanie równoważności
  - Bergstra, J., Ponse, A., Smolka, S., ed. Handbook of Process Algebra, Elsevier, 2001, rozdział 4, rozdział 6, rozdział 9.
  - Stirling, C. Modal and Temporal Properties of Processes, Springer-Verlag, 2001.
Literatura uzupełniająca:
- Inne podejścia niż CCS:
  - M. Hennessy Algebraic Theory of Processes, MIT Press, 1988.
  - C.A.R. Hoare Communicating Sequential Processes, Prentice Hall, 1985.
  - J.C.M. Baeten, W.P. Weijland Process Algebra, CUP, 1990.
  - W. Fokkink Introduction to Process Algebra, Springer Verlag, 1999.
- Zastosowania do specyfikacji i weryfikacji systemów współbieżnych:
  - J.C.M. Beaten, ed. Applications of Process Algebra, CUP, 1990.
  - S. Mauw, G.J. Veltink Algebraic Specification of Communication Protocols, CUP 1993.
Narzędzia
Interesujące strony:
- Metody formalne w WWW Virtual Library
- Systemy wspolbiezne tamze

Egzamin poprawkowy: środa 12 marca 2003, godz. 12:00, pokój 5730