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.