Název:
Formální modely pro práci s datovými jazyky
Překlad názvu:
Formal Models for Data Languages
Autoři:
Vašák, Jan ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce) Typ dokumentu: Bakalářské práce
Rok:
2024
Jazyk:
eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng][cze]
Datová slova jsou běžně používaná pro formální práci se slovy nad nekonečnými abecedami. V praxi může nekonečná abeceda modelovat skutečně nekonečnou množinu, např. celá čísla nebo množinu řeťezců, nebo velkou konečnou množinu, jako např. znaky sady Unicode. Tato práce se nejprve věnuje teoretickým vlastnostem registrově množinových automatů. Registrově množinové automaty jsou modelem nad datovými slovy, který lze použít pro determinizaci velké třídy registrových automatů (toto např. umožňuje deterministickou automatovou reprezentaci třídy regulárních výrazů se zpětnými odkazy). Dále jsme rozšířili streaming data string převaděče, model určený pro modelování třídy programů pro zpracování lineárních seznamů, o množinové registry. Toto rozšíření umožňuje např. modelovat program, který odstraní duplicitní hodnoty z lineárního seznamu, což není možné modelovat základními streaming data string převaděči. Ukážeme, že problém funkční ekvivalence je pro toto rozšíření rozhodnutelný. Také byl naimplementován prototyp regex matcheru založený na registrově množinových automatech. Ukážeme, že prototyp si vede dobře pod ReDoS (regular expression denial of service) útoky, které jsou efektivní vůči regex matcherům používaným v praxi.
Data words are a common way to formally work with words over infinite alphabets. In practice, an infinite alphabet can represent an actually infinite set, such as the integers or a set of strings, or a large finite set, such as the Unicode symbols. We explore some theoretical properties of register set automata, a data word model that, crucially, can be used as a means to determinise a large class of register automata (this allows, e.g., for a deterministic automata representation of a class of regexes with back-references). We also extend streaming data string transducers, a model designed to represent a class of list-processing programs, with set-registers. This extension can, for example, represent a program that removes duplicates from a list, which is not representable using the base model. We then show that this extension’s functional equivalence problem is decidable. Lastly, a prototype regex matcher based on register set automata was implemented, and we experimentally show that it performs well under regular expression denial of service attacks that can cripple other matchers used in practice.
Klíčová slova:
data words; register set automata; regular expressions with back-references; streaming data string transducers; datová slova; registrově množinové automaty; regulární výrazy se zpětnými odkazy; streaming data string převodníky
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: https://hdl.handle.net/11012/246579