Sa~zetak:
Napravit ~te se pregled sintakse i semantike najva~znijih
logik~a s operatorom najve~te (najmanje) ~cvrste to~cke (LFP/GFP,
\mu-ra~cun) i rezimirati njihova osnovna svojstva koja su od va~znosti
u deskriptivnoj teoriji slo~zenosti. Osnovni cilj seminara je
konstruirati odgovaraju~te igre parnosti za verifikaciju modela
u tim logikama, te dokazati korektnost konstrukcije. Zaklju~cit ~te se
s analizom podatkovne, izrazne i kombinirane slo~zenosti
problema verifikacije modela.