Control Strategy Synthesis for Path Planning under Temporal Constraints

Moderni inženýrske systemy jako samořidici auta, bezpilotni letadla, vestavěna zdravotnicka zařizeni a kooperativni systemy mezi clověkem a robotem se vyviji velice rychle podle potřeb průmyslu ale take diky různým akademickým i veřejným soutěžim. Pro mnohe z těchto systemů je bezpecnost kritickou podminkou pro jejich nasazeni v praxi. Proto uměrně rychlemu rozvoji narůsta i potřeba formalnich přistupů k jejich specifikaci, navrhu a verifikaci. Motivaci pro tuto praci je oblast mobilni robotiky a zaměřujeme se na problem planovani cesty, jehož cilem je syntetizovat cestu (s nizkým rozlisenim, na vysoke urovni) nebo řidici strategii pro komplexni dynamický system tak, aby splňovala zadanou specifikaci. Zaměřujeme se specialně na specifikaci zadanou jako formule linearni temporalni logiky (LTL) nad stavy daneho systemu. Pro analýzu takovýchto problemů aplikujeme standardni hierarchický přistup, který umožňuje použiti formalnich metod z informatiky. Tento přistup sestava z abstrakce dynamickeho systemu pomoci diskretniho modelu, syntezy řidici strategie pro tento model a nasledně implementaci řidicich pravidel v původnim dynamickem systemu. S využitim formalnich metod jako ověřovani modelu pomoci automatů a teorie her navrhujeme algoritmy pro syntezu strategii se silnými matematickými vlastnostmi. V prvni casti disertacni prace předpokladame, že již mame k dispozici diskretni model systemu a zaměřujeme se jenom na druhý krok výse uvedeneho hierarchickeho přistupu, a to syntezu řidici strategie. Navrhujeme algoritmy pro deterministicke i pravděpodobnostni systemy, ktere sestroji řidici strategii zarucujici splněni dane LTL formule a zaroveň optimalizuji hodnotu optimalizacni funkce nad (potencialně) měnicimi se a castecně pozorovanými hodnotami objevujicimi se ve stavech systemu, ktere jsou interpretovany buď jako odměny nebo pokuty. Ve druhe casti prace se pak zaměřujeme na obecnějsi problem syntezy řidici strategie pro stochastický linearni dynamický system vzhledem k LTL formuli. Představujeme iterativni algoritmus založený na vylepsovani abstrakce, který modeluje dynamický system pomoci hry dvou a půl hrace, najde výherni strategie pro tuto hru a nasledně pomoci podrobne analýzy teto hry sestroji novou, přesnějsi hru. Vsechny navržene algoritmy byly implementovany a jsou v praci demonstrovany a vyhodnoceny na ilustrativnich přikladech.