Original title: Automaty s komplexními přijímacími podmínkami
Translated title: Automata with complex acceptance conditions
Authors: Bartoš, Petr ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Document type: Master’s theses
Year: 2026
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Tato diplomová práce se zaobírá návrhem automatového modelu, jenž rozšiřuje klasické nedeterministické automaty o barvení jejich stavů. Účelem tohoto modelu je stručná reprezentace opakujících se automatových podstruktur, které vznikají při řešení řetězcových omezení pomocí stabilizační procedury. Navržený model přijímá slova na základě formule popisující barvy, které jsou během běhu automatu pozorovány, což umožňuje reprezentovat více automatů v jednom modelu bez redundance. Práce dále prozkoumává vlastnosti navrženého modelu, představuje algoritmy pro práci s ním a dokazuje správnost a složitost těchto algoritmů. Model je nakonec podroben experimentálnímu testování pomocí problémů z benchmarků SMT-LIB a řešiče Z3-Noodler za účelem posouzení praktické využitelnosti daného modelu. This thesis introduces colored automata, a modification of nondeterministic finite automata designed to compactly represent families of structurally related automata arising in stabilization-based string solving. The proposed model augments automata states with colors and defines acceptance using Boolean combinations of color predicates, allowing shared representation of automata that would otherwise be processed independently. The main goal is to reduce redundant computation caused by repeated exploration of similar automata structures. The thesis formalizes the model, studies its properties, and develops algorithms for fundamental decision procedures. The proposed algorithms are accompanied by correctness proofs and complexity analysis. Finally, the practical applicability of the approach is evaluated experimentally on automata collections derived from SMT-LIB benchmarks and generated using the Z3-Noodler solver.
Keywords: automaty; barevné automaty; barvení stavů; komprese; konečné automaty; SMT; stručnost; verifikace; řetězcová omezení; řešení řetězcových omezení; automata; colored automata; compression; finite automata; SMT; state coloring; string constraint solving; string constraints; succinctness; verification

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/260179

Permalink: http://www.nusl.cz/ntk/nusl-775884


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses