Plánování v pravděpodobnostním prostředí s využitím formálních metod a strojového učení

Předmětem disertační práce bude zejména vývoj teoretických základů pro nové škálovatelné metody řízení systémů  pracujících v pravděpodobnostním prostředí. Zaměříme se na syntézu konečně stavových kontrolérů pro stochastické procesy s částečným pozorováním s využitím pokročilých metod formální kvantitativní analýzy, technikami induktivní syntézy a strojového učení. Práce se rovněž zaměří na využití těchto metod v oblasti řízeních prakticky relevantních pravděpodobnostních systémů, a na důkladné vyhodnocení aplikovatelnosti těchto metod. Výsledky této práce přispějí k pokroku v oblasti automatizace návrhu systémů.

Výzkumu efektivních metod pro syntézu kontrolérů je v současnosti věnována značná pozornost v oblastech formální verifikace, návrhu a implementace programovacích jazyků, umělé inteligence a systémové biologie, o čemž svědčí zaměření řady špičkových konferencí (např. CAV, TACAS, PLDI či CMSB). Syntézou programů a modelů se rovněž zabývá řada velkých projektů na špičkových universitách a výzkumných institucích (např. Berkeley University či Microsoft Research).