Algoritmická analýza stochastických procesů a her

Cílem analýzy systémů reálného světa je automatizovaně odhalovat jejich klíčové vlastnosti. Například systém řízení letového provozu by měl být bezpečný, efektivní a co nejlevnější. Všechny tyto vlastnosti lze algoritmicky analyzovat, pokud se nám podaří vytvořit model onoho systému ve vhodném matematickém formalismu. Každý systém má svá specifika, která je nutné zohlednit při volbě modelovacího jazyka. Mnoho systémů například vykazuje jistou formu nepředvídatelnosti, tzv. kvantifikovanou nejistotu: občas přesně nevíme, v jakém stavu se bude systém nacházet v následujícím okamžiku, ale jsme schopni odhadnout s jakou pravděpodobností se bude nacházet v jednotlivých stavech. Triviálním příkladem je házení mincí: nejsme sice schopni říci, na kterou stranu mince spadne, ale víme, že pravděpodobnost každé ze stran je 1/2 (ignorujeme zde možnost, že mince zůstane stát na hraně).

Obecným formálním modelem systémů, které vykazují prvky kvantifikované nejistoty, jsou stochastické procesy. Mezi nejvíce používané modely patří různé speciální typy Markovových řetězců s diskrétním i spojitým časem. Markovovy řetězce jsou hojně využívány v praxi. Jejich pomocí lze například modelovat chování uživatelů internetu (takový model se stal základem systému Google PageRank), spolehlivosti klientů finančních institucí, populačních procesů v biologii apod. Markovovy řetězce umožňují analýzu mnoha vlastností počínaje výpočtem pravděpodobnosti nekorektního chování až po výpočet průměrné zátěže systému.

Dalším důležitým atributem mnoha reálných systémů je nutnost nějakým způsobem řídit jejich chování. Takové systémy se nacházejí především v oblastech souvisejících s technologiemi a technickou praxí. Důležitou otázkou proto je, zda je možné k danému systému zkonstruovat ovladač, který by jej řídil co nejlépe. Systémy vykazující prvky kvantifikované nejistoty, které navíc umožňují nějakou formu řízení, lze modelovat pomocí tzv. rozhodovacích procesů a stochastických her. Výsledkem analýzy rozhodovacího procesu nebo hry je potom strategie, která dosahuje optimálního výsledku, např. minimalizuje pravděpodobnost srážky letadel a/nebo minimalizuje náklady na provoz řídícího systému.


Hlavní výzkumné směry

  • Rekurzivní stochastické procesy

    Jedná se především o výzkum základních vlastností pravděpodobnostních rozšíření zásobníkových automatů, strojů s čítači, paralelních procesů apod. Naším cílem je studovat základní vlastnosti takových systémů jako např. pravděpodobnost a průměrný čas dosažení dané množiny konfigurací. Obecné výsledky pro rekurzivní procesy je možné aplikovat v mnoha oblastech, např. v teorii front, plánování, v analýze náhodnostních algoritmů, datových struktur apod.

  • Hry více hráčů na přechodových systémech

    V této oblasti se koncentrujeme na řešení speciálního typu tahových her, v nichž má každý hráč vlastní cíl, který není nutně v konfliktu s ostatními (takovým cílem může být například maximalizace pravděpodobnosti dosažení dané množiny stavů). Studujeme základní vlastnosti takových her jako např. existenci rovnovážných situací, složitost výpočtu optimálních strategií apod.

  • Stochastické systémy s reálným časem

    Zejména se jedná o výzkum tzv. zobecněných semi-Markovových procesů (které jsou ekvivalentní stochastickým Petriho sítím). Uvažujeme různé formy specifikace časových limitů pro takové systémy, obvykle pomocí různých variant časových automatů, a také algoritmy pro jejich ověřování.

  • Specifikační formalismy pro stochastické procesy

    Zabýváme se výzkumem fundamentálních vlastností formalismů vhodných pro specifikaci požadovaného chování stochastických procesů. Jedná se zejména o nejrůznější temporální logiky (např. PCTL) a formalismy založené na teorii automatů (např. časové automaty jako specifikační jazyk pro stochastické procesy s reálným časem). Naším cílem je jednak navrhovat vhodné formalismy pro specifikaci klíčových vlastností a jednak navrhovat algoritmy pro ověřování těchto vlastností.


Informace pro studenty

Stochastické procesy a hry jsou velmi živým a atraktivním tématem pro výzkum, do kterého se mohou zapojit i studenti magisterského nebo dokonce bakalářského studia (někteří ze současných doktorských studentů v naší skupině publikovali původní vědecké výsledky ještě během magisterského studia). Problematika je poměrně náročná a je vhodná především pro "matematicky orientované" studenty, kteří hledají vhodnou oblast pro následné doktorské studium. Bližší informace je možné získat od kteréhokoliv člena naší skupiny.


Složení výzkumného týmu


Kontakt

Katedra informačních technologií
prof. RNDr. Antonín Kučera, Ph.D.
Telefon: +420-549 49 4374
Email: tony(atsign)fi(dot)muni(dot)cz
http://www.fi.muni.cz/usr/kucera/
http://iti.fi.muni.cz/


Ocenění získaná členy výzkumného týmu

V přímé souvislosti s aktivitami výzkumného týmu získali jeho členové následující ocenění:
2010 Vojtěch Forejt
Uděleno prestižní stipendium Newton International Fellowship od britské akademie věd, Royal Society
2009 Václav Brožek
Uděleno prestižní stipendium Newton International Fellowship od britské akademie věd, Royal Society
2009 Jan Křetínský
Cena rektora MU nejlepším studentům magisterského studia
2008 Tomáš Brázdil
Beth dissertation award
2008 Vojtěch Forejt
Cena rektora MU nejlepším studentům doktorského studia
2007 Tomáš Brázdil
Uděleno prestižní stipendium Humboldtovy nadace
2007 Tomáš Brázdil
Cena rektora MU nejlepším studentům doktorského studia
2007 Václav Brožek
Cena rektora MU nejlepším studentům magisterského studia
2007 Vojtěch Forejt
2. místo v soutěži SVOČ, kategorie teoretická informatika
2007 Václav Brožek
2. místo v soutěži SVOČ, kategorie teoretická informatika
2003 Tomáš Brázdil
1. místo v soutěži SVOČ, kategorie teoretická informatika