Barbora Šmahlíková získala další prestižní cenu

Barbora Šmahlíková sbírá za svou bakalářskou práci v oblasti omega automatů jedno ocenění za druhým. Po Ceně vlády nadanému studentovi jí udělilo Vienna Center for Logic and Algorithms prestižní mezinárodní ocenění "The Outstanding Undergraduate Thesis Award" za celosvětově nejlepší bakalářskou práci v oblasti formálních metod.

Čím se Barbora zabývá?

Pokud nejste IT odborníci, asi nevíte, co si pod pojmem omega automaty představit. Jedná se o matematický model stojící mimo jiné na pozadí technik, které zajišťují, aby v kritických programech (např. řídících systémů v letadlech, automobilech, satelitech, atp.) nebyly chyby, které by mohly způsobit katastrofickou havárii.

Velmi zjednodušeně řečeno, programátor může ověřit, že jeho program neobsahuje chyby, tak, že si vezme dva slovníky. Jeden slovník bude obsahovat slova, která popisují všechna možná chování programu (v tomto případě bude slovo obsahovat písmena reprezentující různé události v programu, jako je třeba zavolání funkce, zaslání signálu pro katapultování pilota, operace s proměnnými, atp.) a druhý slovník bude obsahovat slova, která popisují všechna správná chování programu. Úkolem je ověřit, zda jsou všechna slova z prvního slovníku obsažena ve druhém slovníku. Pro jedno obyčejné slovo je to jednoduché. V našem případě ale oba slovníky obsahují nekonečně mnoho slov nekonečné délky, což situaci výrazně komplikuje. Omega automaty právě umožňují popis takovýchto nekonečných slovníků nekonečných slov. Ověření správnosti systému pak odpovídá ověření množinové inkluze mezi těmito slovníky.

Obr. 1 Příklad komplementu Büchiho automatu pomocí algoritmu z článku V. Havleny, O. Lengála a B. Šmahlíkové "Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation"; TACAS 2022.
Červené stavy (a stavy, které by z nich následovaly) nebudou díky zavedeným optimalizacím vygenerovány.

V čem je přínos Barbořiny práce?

Jedním z Barbořiných přínosů je optimalizace tzv. rank-based komplementačního algoritmu. Tento základní algoritmus je teoreticky optimální: v nejhorším případě bude na jeho výstupu automat s O((0,76n)^n) stavy (kde n je počet stavů vstupního automatu). Což je zároveň i spodní omezení (tj. existují vstupní automaty, pro které nemůže existovat menší komplement). V praxi se ale této drastické složitosti dá často vyhnout. Výraz (0,76n)^n totiž, zjednodušeně, odpovídá počtu možných surjekcí na n-prvkovou množinu (jde o aproximaci tzv. Stirlingova čísla druhého druhu používaného v kombinatorice), což je struktura, se kterou se v algoritmu pracuje. 

Optimalizace, na jejímž vývoji se Barbora podílela, dokáže na základě strukturálních vlastností vstupního automatu (konkrétně na základě jeho dekompozice do silně souvislých komponent a jejich analýzy, tj, zjištění, jestli jde např. o deterministické či inherentně slabé komponenty) snížit velikost oboru hodnot surjekcí, a tím kombinatoricky snížit velikost vygenerovaného automatu.

Obr. 2 [vlevo:] Příklad Büchiho automatu. [vpravo:] Komplement Büchiho automatu z obrázku vlevo pomocí techniky založené na dekompozici automatu na silně souvislé komponenty z článku V. Havleny, O. Lengála, Y. Lii, B. Šmahlíkové a A. Turrini: "Modular Mix-and-Match Complementation of Büchi Automata"; TACAS 2023.
Výstupní automat má v tomto případě obecnější, tzv. Emeron-Lei, příjímající podmínku.

Vědecká práce od začátku studia

Barbora začala se svým výzkumem ve 2. ročníku bakalářského studia v rámci předmětu Projektová praxe s Vojtěchem Havlenou a Ondřejem Lengálem ze skupiny VeriFIT. V září bude nastupovat do druhého ročníku magisterského studia. Během těchto tří let se významně podílela na čtyřech článcích na mezinárodních konferencích, z nichž tři jsou v dané oblasti považovány za špičkové.

O významu ocenění svědčí i fakt, že Vienna Center for Logic and Algorithms (VCLA) je jednou z nejprestižnějších organizací zabývajících se logikou a formálními metodami ve světě. Ocenění za celosvětově nejlepší bakalářskou a magisterskou práci v oblasti formálních metod letos udělila po sedmé.