Шабана Ханан Магди Дарвиш Синхронизация частичных и недетерминированных автоматов: подход на основе sat-решателей

Краткое описание

Шабана Ханан Магди Дарвиш Синхронизация частичных и недетерминированных автоматов: подход на основе sat-решателей
ОГЛАВЛЕНИЕ ДИССЕРТАЦИИ
кандидат наук Шабана Ханан Магди Дарвиш
Contents

Introduction

Relevance of the topic

Degree of development of the topic

Goals and objectives of the thesis. SAT-solver method

Overview of the thesis

The main achievements of the thesis

Publications

Approbation at seminars and conferences

Scientific novelty

Degree of correctness of the results

Theoretical and practical importance

Research methods

Length and structure of thesis

Acknowledgments

1 Preliminaries

1.1 Complexity classes

1.2 Satisfiability

1.3 Finite automata

1.4 Synchronizing DFA

1.5 NFA Synchronization

1.6 Complexity of synchronization

in finite automata

1.7 Shortest synchronizing word

1.7.1 Shortest synchronizing word for DFAs

1.7.2 Shortest synchronizing word for NFA

1.8 Careful synchronization

1.9 Exact synchronization

1.10 Checking careful synchronization

1.11 Testing exact synchronization

2 Synchronization of PFAs

2.1 Carefully synchronizing words

2.2 Exactly synchronizing words

2.3 Ladder encoding

3 Experimental study in PFAs synchronization

3.1 General settings of our experiments

3.2 Experiments and implementation

3.3 Generating random PFAs

3.4 Experimental results for randomly

generated PFAs and their analysis

3.4.1 Series 1: Probability of synchronization

3.4.2 Series 2: Average length of the shortest synchronizing word

3.4.3 Series 3: Influence of the input alphabet size

3.4.4 Series 4: Influence of density

3.5 Slowly synchronizing automata

and benchmarks

3.6 A comparison with the partial power automaton method

4 Synchronization problems of NFAs

4.1 Modeling NFA computation as SAT:

Variables

4.2 Modeling NFA computation as SAT: Clauses

4.3 Propositional logic formulas for rules

4.4 CNF formulas

4.5 NFA-synchronization problems

4.5.1 D3-synchronization

4.5.2 D2 synchronization

4.5.3 Di-synchronization

4.6 Example of the CNF table

for DiW problems

5 Experiments in NFA synchronization

5.1 NFA Generation

5.2 Uniform Model results

5.3 Poisson Model results

5.3.1 D3 results

5.3.2 D2 results

5.4 Enhancement of the algorithm

Conclusion

Bibliography