Cílem práce je vývoj prototypového nástroje pro efektivní analýzu deterministických spojitých modelů dynamických systémů s neurčitostí výchozích podmínek. Uvažované modely budou zohledňovat doménu populační kinetiky biologických systémů, jedná se o autonomní nelineární diferenciální rovnice prvního řádu. Navrhované řešení bude postaveno na technologii ověřování modelů adaptované pro diskrétní časové řady (získané z numerických simulací případně experimentů).

Konkrétní cíle práce:

1. Navrhnout a implementovat prototyp nástroje, který zajistí efektivní ověření, zda-li množina časových řad výchazejících z různých inicálních bodů splňuje specifikaci zadanou ve formě lineární temporální formule s omezeními definovanými jako nerovnosti v doméně reálných čísel.
2. Evaluovat prototypové řešení na několika dynamických modelech. Výstupem evaluace bude identifikace kritických částí vhodných pro případnou akceleraci na technologii GPU.

Algoritmické řešení bude vycházet z metody bounded model checking (Biere et.al.) a známých algoritmů pro detekci cyklů. Výběr vhodných algoritmů a adaptace metody model checkingu je součástí vlastní práce studenta (teoretická část).

Jazykem implementace bude Python, pro numerické simulace bude použito dostupných nástrojů (NumPy, SimPy-LSODA).

Očekávané výstupy:

1. zdrojové kódy a stručná dokumentace (spuštění, popis vstupů, parametrů, výstupů)
2. evaluace zpracována vizuální formou (grafy), evaluační data mohou být součástí přílohy