D. Niwinski: Rachunek Mi

Damian Niwinski

Rachunek Mi

Rachunek Mi jest, najogolniej mowiac, algebra monotonicznych funkcji nad krata zupelna,
gdzie bazowymi operacjami sa zlozenie oraz operatory najmniejszego i najwiekszego punktu stalego.
W pewnym sensie rachunek Mi uogolnia pojecie indukcyjnej definicji, powszechnie stosowane w matematyce.

Rachunek Mi wylonil sie z logiki matematycznej i teoretycznej informatyki, obecnie jest uwazany za jeden z najlepszych
formalizmow do automatycznej weryfikacji systemow przy pomocy metody ``model checking''.

W wykladzie przedstawione zostaly podstawowe prawa rachunku Mi oraz jego semantyka w terminach nieskonczonych gier.
Wykazano takze, ze alternacja najmniejszego i najwiekszego punktu stalego prowadzi do istotnie nieskonczonej hierarchii.

Tematy zaliczeniowe .
Notatki z poczatkowych wykladow (Rafal Rusin).
Literatura
- A.Arnold, D.Niwinski, Rudiments of Mu-calculus.
- D.Niwinski, Fixed point characterization of infinite behavior of finite state systems (1997).
- D.Niwinski, Mu-calculus via games (2002).
- I.Walukiewicz, Notes on the Propositional Mu-Calculus: Completeness and related results (1995).
- I.Walukiewicz, Automata and logic (EEF Summer School 2001).