Není automat jako automat. Studentka FIT pomocí Büchiho automatů vylepšuje analýzu programů

Jméno Barbory Šmahlíkové, studentky Fakulty informačních technologií VUT, posledního půl roku v její branži velmi rezonuje. Povedlo se jí totiž zdokonalit algoritmus pro Büchiho automaty. Výrazně tím zlepšila efektivitu výpočtu jejich komplementace, která může sloužit například k terminační analýze programů.

V současné době je její vylepšený algoritmus dokonce považován za jeden z celosvětově nejlepších. Za svou práci ji 27. ledna 2023 Rada pro výzkum, vývoj a inovace (RVVI) jmenovala nositelkou Ceny vlády nadanému studentovi. Ocenění si převzala ve čtvrtek 8. června v Hrzánském paláci Praze. Na Akademickém shromáždění v roce 2022 také získala Cenu rektora, dále obdržela Cenu Zdeny Rábové a dostala se do finální sestavy soutěžících v univerzitní soutěži 8 z VUT.

Do výzkumu se pustila skoro už na začátku bakalářského studia a k tématu bakalářské práce přišla téměř jako slepý k houslím, protože jí bylo přiděleno. „Rozhodně jsem neměla jasnou představu, čím bych se chtěla zabývat. Jediné, co jsem věděla, bylo, že bych chtěla zkusit pracovat ve výzkumu a zároveň se věnovat něčemu souvisejícímu s matematikou. Pak jsem se dozvěděla o možnosti zapojit se, ale neměla jsem na to odvahu. Neuměla jsem si představit, že bych sama něco dokázala vymyslet. Pak mě ale přímo oslovili, tak jsem se nakonec zapojila a v tématu se našla – i když mi trvalo přes půl roku, než jsem algoritmus pochopila natolik, abych jej mohla vylepšit,“ popisuje Barbora. V tématu se rozhodla pokračovat a věnovala se mu ve své bakalářské práci.

Její práce v oblasti vývoje algoritmů pro tzv. omega automaty brzy vyústila v publikace na mezinárodních konferenčních fórech, která jsou převážně vyhrazeny doktorským studentům. A v čem přesně spočívá kouzlo Büchiho automatů? Jedná se o abstraktní model, pomocí kterého je možné namodelovat nějaký systém, na němž je poté možné sledovat některé jeho vlastnosti. „Mám jeden hlavní automat pro systém řekněme model A a chci otestovat nějakou jeho vlastnost. Vytvořím si tedy automat B pro tuto vlastnost a s využitím komplementace můžu ověřit, zda tato vlastnost pro systém platí, nebo ne,“ vysvětluje Barbora. „Takhle můžeme například ověřit, že se nějaký program, například operační systém, počítačová hra apod. nikdy nezasekne,“ dodává.

Může ale existovat takové obrovské množství možností, jakým způsobem se systém může chovat, že hrozí, že by počítači mohla dojít paměť dříve, než by bylo možné zjistit, zda program splňuje tu danou vlastnost, kterou jsme testovali. Proto je zapotřebí, aby byl algoritmus co nejefektivnější a nevyužíval tolik paměti.Toho lze dosáhnout právě nějakými optimalizacemi, kterými se Barbora zabývá.

Barbora na algoritmu stále pracuje, přičemž zkoumá i další automaty – teď se zabývá i se ELA automaty, které fungují na podobném principu. To, co by šlo pomocí Büchiho automatů reprezentovat složitě, se pomocí ELA automatů dá reprezentovat jednodušeji. Zkoumá tedy další metodu, která by do budoucna mohla být ještě efektivnější.