|
|
Efektivní algoritmy pro práci s Büchiho automaty
Laščák, Tomáš ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je rozšířit existující knihovnu VATA o modul pro práci s Büchiho automaty, které se řadí mezi konečně stavové automaty nad nekonečnými slovy. Tyto automaty jsou využívány v různých oblastech informatiky, mimo jiné také ve formální verifikaci, při LTL model checkingu. LTL model checking se provádí typicky za pomocí operace testování jazykové inkluze mezi dvěma Büchiho automaty. Protože jazyková inkluze může být výpočetně velmi náročná, vzniklo několik optimalizovaných algoritmů pro tento problém, jako je například přístup založený na Ramseyho větě. Předkládaná práce je zaměřena na tento přístup, jehož implementace je přidána do nově vytvořeného rozšíření knihovny VATA. Mimo to jsou do tohoto nového rozšíření přidány také další operace nad Büchiho automaty, jako jsou sjednocení, průnik nebo redukce počtu stavů.
|
|
|
Algoritmy pro segmentaci webových stránek
Laščák, Tomáš ; Burgetová, Ivana (oponent) ; Burget, Radek (vedoucí práce)
Segmentace webových stránek je jednou z disciplín extrakce informací. Umožňuje dělit stránky na různé sémantické bloky. Diplomová práce se zabývá seznámením se samotnou segmentací a také implementací konkrétní segmentační metody. V práci jsou popsány různé příklady metod jako je VIPS, DOM PS atd. Je zde teoretický popis zvolené metody a taktéž Frameworku FitLayout, který bude o tuto metodu rozšířen. Dále je tu podrobněji popsaná implementace zvolené metody. Popis implementace je zaměřen především na popis různých problémů, které jsme museli vyřešit. Nechybí zde ani testování, které pomohlo odhalit některé nedostatky. V závěru se nachází shrnutí výsledků a možné nápady, jak by se dalo navázat na tuto práci.
|
|
|
Efektivní algoritmy pro práci s Büchiho automaty
Laščák, Tomáš ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je rozšířit existující knihovnu VATA o modul pro práci s Büchiho automaty, které se řadí mezi konečně stavové automaty nad nekonečnými slovy. Tyto automaty jsou využívány v různých oblastech informatiky, mimo jiné také ve formální verifikaci, při LTL model checkingu. LTL model checking se provádí typicky za pomocí operace testování jazykové inkluze mezi dvěma Büchiho automaty. Protože jazyková inkluze může být výpočetně velmi náročná, vzniklo několik optimalizovaných algoritmů pro tento problém, jako je například přístup založený na Ramseyho větě. Předkládaná práce je zaměřena na tento přístup, jehož implementace je přidána do nově vytvořeného rozšíření knihovny VATA. Mimo to jsou do tohoto nového rozšíření přidány také další operace nad Büchiho automaty, jako jsou sjednocení, průnik nebo redukce počtu stavů.
|
|
|
Algoritmy pro segmentaci webových stránek
Laščák, Tomáš ; Burgetová, Ivana (oponent) ; Burget, Radek (vedoucí práce)
Segmentace webových stránek je jednou z disciplín extrakce informací. Umožňuje dělit stránky na různé sémantické bloky. Diplomová práce se zabývá seznámením se samotnou segmentací a také implementací konkrétní segmentační metody. V práci jsou popsány různé příklady metod jako je VIPS, DOM PS atd. Je zde teoretický popis zvolené metody a taktéž Frameworku FitLayout, který bude o tuto metodu rozšířen. Dále je tu podrobněji popsaná implementace zvolené metody. Popis implementace je zaměřen především na popis různých problémů, které jsme museli vyřešit. Nechybí zde ani testování, které pomohlo odhalit některé nedostatky. V závěru se nachází shrnutí výsledků a možné nápady, jak by se dalo navázat na tuto práci.
|
host ::
RSS.