|
|
Transducers in Automata Library Mata
Chocholatý, David ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
We implement finite transducers in a new fast and simple automata library Mata. Finite transducers are finite state machines modelling rational relations. Our primary use case for finite transducers is encoding replace operations (replacing a word or a regular pattern with a string literal). A recent automata-based SMT string solver Z3-Noodler uses Mata as a backbone of its decision procedure. Z3-Noodler needs finite transducers to analyse string manipulating programs with replace operations. The analysis of said programs used in web applications prevents software attacks such as cross-site scripting (XSS) or code injection. The distinctive features of Mata include simplicity (simple to use, modify and extend) and efficiency (fast to run). We design the representation and algorithms for finite transducers to fit the simplicity and efficiency requirements. We inherit and extend the existing data structures and algorithms for finite automata in Mata to represent the finite transducers and their operations. The representation for finite transducers serves as a common data structure and interface for the finite transducers and future representation of automata using multi-terminal binary decision diagrams to handle large alphabets. We further extend the design with algorithms to construct finite transducers modelling replace operations defined in SMT-LIB. Finally, we run an experimental evaluation of performance of finite transducers in Mata on a new benchmark with replace operations from runs of Z3-Noodler and from solving problems in pattern matching.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (oponent) ; Holík, Lukáš (vedoucí práce)
We explore possibilities of using various abstractions of finite automata languages in optimization of automata algorithms used in automata reasoning. We focus on abstracting languages of states to sets of accepted lengths of word or Parikh images, represented as semi-linear sets, and explore options of using them to optimize automata constructions by pruning states based on abstractions of their languages. We propose several abstractions and work on optimizing their performance. We use two common finite automata problems, synchronous product construction and deciding the emptiness of finite automata intersection, as benchmark problems on which we test our optimizations. Nevertheless, our abstractions are applicable on many other typical automata operations, e.g., complement generation etc. Our experiments show that the proposed optimizations reduce generated state space for both benchmark problems substantially.
|
|
|
Regulované jazykové operace a jejich užití
Chocholatý, David ; Kožár, Tomáš (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce představuje a studuje vymazávací systémy jako alternativní formální jazykový model k obecným skákajícím konečným automatům. Významným rozdílem oproti daným automatům je využití řídícího regulárního jazyka namísto stavového řízení v podobě obecného konečného automatu. Vymazávací systémy ponechávají práci s řetězci na vstupní pásce, přičemž samotné regulární jazyky mohou být přijímány klasickými konečnými automaty. Zároveň se zavedením nového formálního systému práce prokazuje jeho vztahy se známými jazykovými rodinami, rodinou jazyků zamíchání, Dyckovými jazyky a uzávěrové vlastnosti. Na základě formální specifikace vymazávacího systému je uvedeno více aplikací v oblasti bioinformatiky pro molekulární biologii, textových editorů a kompozičního šachu, včetně návrhu algoritmů a prezentování implementačního řešení.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (oponent) ; Holík, Lukáš (vedoucí práce)
We explore possibilities of using various abstractions of finite automata languages in optimization of automata algorithms used in automata reasoning. We focus on abstracting languages of states to sets of accepted lengths of word or Parikh images, represented as semi-linear sets, and explore options of using them to optimize automata constructions by pruning states based on abstractions of their languages. We propose several abstractions and work on optimizing their performance. We use two common finite automata problems, synchronous product construction and deciding the emptiness of finite automata intersection, as benchmark problems on which we test our optimizations. Nevertheless, our abstractions are applicable on many other typical automata operations, e.g., complement generation etc. Our experiments show that the proposed optimizations reduce generated state space for both benchmark problems substantially.
|
host ::
RSS.