National Repository of Grey Literature 2 records found  Search took 0.00 seconds. 
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Komplementace Büchiho automatů je klíčovou operací pro terminační analýzu programů, model checking nebo rozhodovací procedury pro různé logiky. Tato práce se zabývá především optimalizacemi rank-based komplementace Büchiho automatů. Původní rank-based algoritmus je sice asymptoticky optimální, přesto může generovat nezbytně velký stavový prostor. Pro praktické použití je tedy žádoucí maximálně redukovat počet vygenerovaných stavů v komplementu. V této práci představíme několik technik pro efektivní komplementaci některých speciálních typů Büchiho automatů, často se vyskytujících v praxi, které jsou založené na jejich struktuře. Některé z navržených technik lze do určité míry rozšířit i pro obecné Büchiho automaty. Techniky představené v této práci byly implementovány jako rozšíření nástroje Ranker pro komplementaci Büchiho automatů. Tyto optimalizace výrazně redukují generovaný stavový prostor a Ranker ve většině případů produkuje menší komplement než ostatní existující nástroje pro komplementaci.
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Komplementace Büchiho automatů je klíčovou operací pro terminační analýzu programů, model checking nebo rozhodovací procedury pro různé logiky. Tato práce se zabývá především optimalizacemi rank-based komplementace Büchiho automatů. Původní rank-based algoritmus je sice asymptoticky optimální, přesto může generovat nezbytně velký stavový prostor. Pro praktické použití je tedy žádoucí maximálně redukovat počet vygenerovaných stavů v komplementu. V této práci představíme několik technik pro efektivní komplementaci některých speciálních typů Büchiho automatů, často se vyskytujících v praxi, které jsou založené na jejich struktuře. Některé z navržených technik lze do určité míry rozšířit i pro obecné Büchiho automaty. Techniky představené v této práci byly implementovány jako rozšíření nástroje Ranker pro komplementaci Büchiho automatů. Tyto optimalizace výrazně redukují generovaný stavový prostor a Ranker ve většině případů produkuje menší komplement než ostatní existující nástroje pro komplementaci.

Interested in being notified about new results for this query?
Subscribe to the RSS feed.