Táto práca sa zaoberá špecifikáciou oscilačných vlastností a
ich analýzou na vybraných modeloch. Konkrétne ide o dva modely
cirkadiálnych rytmov siníc a dva minimálne modely oscilácií.
Východiskom je ich prepis do jazyka BioNetGen Language (BNGL).
Práca obsahuje prehľad vybraných techník pre formálnu
špecifikáciu a analýzu oscilačných vlastností. Základné
vlastnosti oscilácií sú definované najmä pomocou temporálnej
logiky, konkrétne pomocou formúl LTL, STL a STL*. Práca sa
zaoberá rozdelením, popisom, ale aj možnosťami využitia a
základnou demonštráciou definovaných vlastností. Následne boli
tieto vlastnosti pomocou vybraných aplikácií na uvedených
modeloch analyzované, zahŕňajúc aj výkonnostné aspekty.