Synchronization of partial and non-deterministic automata: a sat-based approach : dissertation for the degree of candidate of physical and mathematical sciences : 05.13.17

Relevance of the topic
Finite automata are mathematical models for a lot of discrete dynami- cal systems arising in robotics, communication protocols, biology, com- puter hardware design, artificial intelligence, linguistics, and other areas. These systems are known as finite-state transition systems. Such a sys- tem consists of a finite number of states and transitions rules. The state of the system at any moment of time is changed, responding to exter- nal input. The transitions rules determine the transition between those states, according to the input.
In the design of the control systems modeled by finite automata, the essential behavior of the finite automaton is the mapping of external sequences into internal states. When for some reasons the automaton fails to take the correct transition (there is a failure in the system), the person responsible of the system decides to direct the system to a known state from which he or she can restore control over the system. He or she can do that if and only if the system is synchronizing. Hence, synchronization is a significant concept for a lot of systems as it makes the systems more robust.
5
Introduction
Synchronization frequently appears in the following situation. Sup- pose that a system is composed of sub-systems that work as identical mechanisms but may be in different states. For some reason, we want all of these sub-systems to be at the same state at the same time. This task can be easily accomplished if the given system is synchronizing. In this situation we can say that the synchronization of a system means that all parts of the system are in agreement regarding the present state of the system.
Now we switch from an informal discussion of synchronization to precise definitions. An automaton is defined as a triple ⟨Q, Σ, δ⟩ where Q is the state set, Σ is the input alphabet and δ is the transition function that defines the action of elements of Σ on the elements of Q. The result of the action of an input letter a ∈ Σ at a state q ∈ Q is denoted as δ(q, a) (or q.a for simplicity). This action is naturally extended to define the action of a word in Σ∗ at any state in Q. (Here Σ∗ stands for the set of all words over the alphabet Σ, including the empty word.) We do not need to specify initial nor final states of the automaton as the study of synchronization considers, in a sense, all states being initial and final.
An automaton is synchronizing if it has an input word that brings it to a unique state regardless of the state of the automaton before reading this word. Figure 1 shows an example of a synchronizing automaton with four states 0, 1, 2, 3 and two input letters a and b. It is easy to verify that the word baaa transfers the automaton from any state to state 0. Such a word is called a synchronizing word or a reset word.
6

Introduction
a
0b1 b
a,b b a 3a2
Figure 1: A synchronizing automaton
The concept of synchronizing words for finite automata has received lots of attention during the last years as they appear in a wide range of applications. Here we briefly describe a few examples of such applica- tions.
Industrial robotics. Synchronizing words reset the automaton to a unique state regardless of its present state. These words are useful in industrial robotics see [30,61,62]. In such industrial issues, synchronizing automata are widely used to model and design feeders, sorters, and ori- enters that work with flows of certain objects carried by a conveyer. We borrow an illustrative example from [2]. Consider an automatic line for manufacturing of a device. Suppose a certain part of the device has the shape shown in Figure 2. Such parts arrive to the conveyer in random orientations. These different orientations of the part are illustrated in Figure 3. For assembly these parts need to be oriented in the same way. Assume that each part needs to be in the second (from the left) position from Figure 3.
7

Introduction
Thus, one has to design an orienter that senses the position of the incoming part and then rotates it to the prescribed position. Generally speaking, such an orienter is complicated as its mechanism is dependent on the shape of the part. Practical considerations favor methods which require little or no sensing, employ simple tools, and are as robust as possible. The desired orienter is one whose processing is independent of the initial orientation of the part. Now we quote from [2]. “For our particular case, these goals can be achieved as follows. We put parts to be oriented on a conveyer belt which takes them to the assembly point and let the stream of the parts encounter a series of passive obstacles placed along the belt. We need two type of obstacles: tall (T) and short (S). A tall obstacle should be tall enough in order that any part on the belt encounters this obstacle by its rightmost low angle (we assume that the belt is moving from left to right). Being carried by the belt, the part then is forced to turn 90◦ clockwise as shown in Figure 4. A short obstacle has the same effect whenever the part is in the ‘bump-down’ orientation (the first from the left in Figure 3); otherwise it does not touch the part which therefore passes by without changing the orientation”. Thus, we can construct the orienter as an automaton A whose state set consists of the different orientations, whose input alphabet is {T,S}, and whose transition function is defined by the action of each obstacle on different orientations of the part. The automaton A is described in Figure 5. It is easy to verify that this automaton is synchronizing and the sequence S–T–T–T–S–T–T–T–S of obstacles is a synchronizing word that yields the desired sensorless orienter.
8

Figure 3: Four possible orientations; the “correct” orientation is the sec- ond one from the left.
Introduction
Figure 2: A polygonal part
❅❅
Figure 4: The action of a tall obstacle
T,S
S TT
STS Figure 5: Sensorless orienter A
9
❅❅
❅❅

Introduction
Coding theory. A word u over an alphabet Σ is said to be a prefix of awordwoverΣifwcanbewrittenasw=uvforsomev∈Σ∗. Aprefix code X over Σ is a set of non-empty words from Σ∗ such that no word of X is a prefix of another word of X. It is maximal if it is not contained in another prefix code over the same alphabet. A maximal prefix code X over Σ is called synchronized if there is a word z such that for any word y ∈ Σ∗, the word yz can be decomposed as a product of words from X. Such a word z is called a synchronizing word for X. When coding a stream of data with a synchronized code, we have a guarantee that we can recover after a loss of synchronization between the decoder and the coder caused by channel errors [9]. In the case of such a loss, it suffices to transmit a synchronizing word and the following symbols will be decoded correctly. Moreover, this may happen automatically when a sufficiently long word has been read. For synchronizing codes, the probability that a word w ∈ Σ∗ contains a synchronizing word as a factor tends to 1 as the length of w increases [13].
For an illustration, we consider the following example from [42]. Let Σ = {0,1} and X = {000,0010,0011,010,0110,0111,10,110,111}. Then X is a maximal prefix code over Σ and it is easy to check that each of the words 010, 011110, 011111110, . . . is a synchronizing word for X. For instance, if the code word 000 has been sent but, due to a channel error, the word 100 has been received, the decoder interprets 10 as a code word, and thus, loses synchronization. However, with a high probability this synchronization loss only propagates for a short while; in particular, the decoder definitely re-synchronizes as soon as it encounters one of the segments 010, 011110, 011111110, . . . in the re- ceived stream of symbols. A few samples of such streams are shown in
10

Introduction
Figure 6, where vertical lines show the partition of each stream into code words and the boldfaced code words indicate the position at which the decoder re-synchronizes.
Sent 000 |0010 |0111|…
Received 10|000|10|0111|…
Sent 000|0111|110|0011|000|10|110|… Received 10|0011|111|000|110|0010|110|… Sent 000|000|111|10|…
Received 10|000|0111|10|…
Figure 6: Automatic synchronization
There is a strong connection between codes and finite automata, see the monograph [9] for an extensive treatment. Here we limit ourselves to just one example of such a connection. If X is a finite maximal prefix code over an alphabet Σ, then its decoding can be implemented by a finite automaton AX whose set of states Q is the set of all proper prefixes of the words in X (including the empty word ε) and whose transitions are definedasfollows: forq∈Qanda∈Σ,
q.a= qa ifqaisaproperprefixofawordofX, ε if qa ∈ X,
X is a synchronized code if and only if the automaton AX has a syn- chronizing word that resets it to the state ε.
11

Introduction
Model based testing. Other problems for which synchronizing au- tomata and synchronizing words are important can be found in model conformance testing [8,16,51,52]. These problems consist of some test- ings to ensure that a system verifies its prerequisites. When the abstract behavior of an interactive system is implemented by finite automata, there are various methods to derive some test sequences with high fault coverage. These methods construct a test sequence to be applied when the implementation under test (IUT) is in a certain state. Therefore it is required to bring the IUT to this particular state regardless of its initial state which can be accomplished by using a synchronizing sequence for the IUT. Figure 7 shows the general technique of model based testing process.
synchronizing word
Figure 7: Model based testing process
A popular automata model in the area of model based testing is the finite state machine (FSM) model, see, e.g., [45–50,89,90]. A FSM is basically a nondeterministic automaton with output, and a common
12
Output: Pass or fail
Test gener- ating tools
Initial IUT
Test Suit
Response
Reset IUT

Introduction
restriction to FSMs used in model based testing is observability: a FSM F with input alphabet I and output alphabet O is said to be observable if for each state q of F and for each input/output pair (i, o) ∈ I × O, at most one action of the input i at q produces the output o. It is easy to see that from the synchronization viewpoint, such an observable FSM is equivalent to a partial automaton with the same state set and the alphabet Σ = I × O.
We think that this brief survey suffices to support the claim that synchronizing automata serve as simple yet adequate models of error- resistant systems in many applied areas. At the same time, synchroniz- ing automata surprisingly arise in some parts of pure mathematics and theoretical computer science (symbolic dynamics, theory of substitution systems, formal language theory). From both applied and theoretical viewpoints, the key question is to find the optimal, i.e., shortest syn- chronizing word for a given synchronizing automaton. Under standard assumptions of complexity theory, this optimization question is known to be computationally hard. As it is quite common for hard problems of applied importance, there have been many attempts to develop practical approaches to the question. These approaches have been based on cer- tain heuristics [1,39–41] and/or popular techniques, including (but not limiting to) binary decision diagrams [68], genetic and evolutionary al- gorithms [44,73], satisfiability solvers [77], answer set programming [32], hierarchical classifiers [69], and machine learning [70].
13

Degree of development of the topic
So far, most of the published research on synchronization has focused on systems that are modeled as complete deterministic automata (DFAs). We refer to the survey [88] and the chapter [42] of the forthcoming ‘Hand- book of Automata Theory’ for a discussion of synchronizing complete deterministic automata as well as their diverse connections and appli- cations. In such systems a full specification of the system is provided; response of the system to any input is uniquely determined by the cur- rent state and the incoming input. Recently a great deal of attention has also been given to synchronization of partially specified systems, in which only a subset of the system’s events are available for external ob- servation. These systems are also known as nondeterministic systems. In such systems, the knowledge of the current state and the incoming input is insufficient to uniquely determine the next state. Such non- determinism arises due to un-modeled system dynamics and/or partial observation. For example, a machine in a manufacturing system may in- cur a partial undetectable failure while performing a certain task. This can be modeled by having a nondeterministic transition on the task com- pletion event, leading to two successor states depending on whether or not the failure occurred while completing the task. Other kind of non- deterministic systems is partial deterministic system in which there are some events that are not allowed for some states. Complete deterministic automata cannot be used in modeling partially specified systems. For these systems, other classes of automata are used: nondeterministic au- tomata (NFAs) and partial deterministic automata (PFAs). Nowadays, synchronization of these automata has become an interesting research topic.
14
Introduction

Goals and objectives of the thesis. SAT-solver method
In this thesis we focus on the case of partial and nondetermin- istic automata. We investigate synchronization of these automata. In contrast to synchronization of complete deterministic automata, syn- chronization problems for nondeterministic or even partial deterministic automata are much harder. For these automata, there is more than one version of synchronization. An automaton may be synchronizing with re- spect to one version but not synchronizing from the view point of another version.
Some of problems that are frequently asked in this area are:
1. For a version of synchronization B, is a given automaton A syn-
chronizing with respect to B?
2. Can we solve Problem 1 in polynomial time as for complete deter-
ministic automata?
3. How does the degree of nondeterminism in A affect being synchro- nizing?
4. If the automaton A already belongs to B, does it have a synchro- nizing word of a specified length?
5. What is the length of the shortest synchronizing word for A ?
6. For synchronizing nondeterministic or partial deterministic au- tomata with a given number of states, what is the average length of their shortest synchronizing words?
15
Introduction

Introduction
In the literature, there are two methods to solve the above prob- lems. The basic one is the power automaton method. It is based on the classical construction of power automata due to Rabin and Scott [71]. This method has delivered many important theoretical results but it is not efficient in practice as the power automaton has an exponential size compared to the size of the input automaton. The second method uses the deterministic automata as tools to solve these problems. Since the synchronization of deterministic automata is extensively studied and up- per bounds or the exact length of the shortest synchronizing word for various kinds of such automata are given, there were attempts to solve Problems 3-6 by certain reductions to complete deterministic automata; see [35] and [37] for details. Although these attempts have proved their efficiency in complete nondeterministic automata for a certain version of synchronization, they can not be applied to other versions of synchro- nization.
In accordance to the hardness of these problems, our motivation was to find tools that have proved to be powerful in dealing with compu- tationally hard issues. Such tools are provided in particular, by SAT solvers; these are computer programs designed to solve the Boolean sat- isfiability problem (SAT).
SAT is a decision problem in propositional logic on a set of variables V and clauses C. The question is: is there a Boolean assignment for V that satisfies all clauses in C? Modern SAT-solvers can solve such decision problems with millions of variables and clauses in a few minutes. Due to this advantage, the following approach to computationally hard problems has become quite popular nowadays: one encodes instances of such problems into instances of SAT that are then fed to a SAT solver.
16

Introduction
We refer to this approach as the SAT-solver method. SAT-solver method has proved to be very efficient for an extremely wide range of problems of both theoretical and practical importance. Its applications are far too numerous to be listed here; we refer the reader to the survey [29] or to the handbook [6] for some examples of successful applications of SAT-solver method in various areas.
Here we mention only three recent papers that deal with two difficult problems related to finite automata. Geldenhuys, van der Merwe, and van Zijl [26] have used the SAT-solver method to attack the minimization problem for NFAs. In the minimization problem, which is known to be PSPACE-complete [38], an NFA A with designated initial and final states is given, and one looks for an NFA of minimum size that accepts the same set of words as A . Skvortsov and Tipikin [77] have applied the method to find a synchronizing word of minimum length for a given complete deterministic automaton (DFA) with two input symbols, and Gu ̈ni ̧cen, Erdem, and Yenigu ̈n [32] have extended their approach to DFAs with arbitrary input alphabets. The problem of finding a synchronizing word of minimum length is known to be hard for the complexity class FPNP[log], the functional analogue of the class of problems solvable by a deterministic polynomial-time Turing machine that has an access to an oracle for an NP-complete problem, with the number of queries being logarithmic in the size of the input [65].
It should be stressed that neither the encoding of NFAs used in [26] nor the encoding of synchronization used in [32,77] work for our purposes. Therefore, we have had to invent essentially different encodings specific for the problems addressed in the thesis.
17

Overview of the thesis
In Chapter 1 we give an overview of relevant aspects related to syn- chronization of automata. In order to place our research in a proper per- spective, we start by synchronization of fully specified automata (com- plete deterministic automata). Then we switch to the nondeterminis- tic automata where we give a survey on the synchronization issues and overview results of recent papers published in this area. From this dis- cussion we conclude that Problem 1 above is PSPACE-complete and hence the answer to Problem 2 is NO in general. Consequently all the remaining problems are computationally hard.
Chapter 2 investigates synchronization of partial deterministic au- tomata (PFAs). For these automata there are two versions of synchro- nizations called Careful and Exact synchronization. We introduce en- codings that model these versions of synchronization as SAT problems. The main results of the chapter are Theorem 2.1 and Theorem 2.2 that prove the adequacy of these encodings.
Chapter 3 presents an experimental study of synchronization of PFAs. We performed a series of experiments to find an approximation of the shortest synchronizing word for a given automaton in each version. It also shows the probability of being synchronizing for each version. The results of another series of experiments is presented. These results show the influence of increasing partiality in the automaton on the syn- chronization and the length of the shortest synchronizing word for each version. At the end of chapter we give some of benchmarks used to prove the efficiency of our algorithm comparing to the other known algorithms. The experiments have also allowed us to find two new infinite series of slowly synchronizing partial deterministic automata. The results of our
18
Introduction

Introduction
algorithm match the result of brute-force algorithm in [86]; the latter algorithm is used only for one version of synchronization. Along with experimental results and their discussion, the chapter also contains two theoretical results: Proposition 3.3 and Proposition 3.4 that find the exact length of the shortest synchronizing word for two series of slowly synchronizing partial deterministic automata.
Chapter 4 studies the synchronization problems in nondetermin- istic automata. Synchronization of nondeterministic automata is more complicated than that of partial deterministic automata since the lat- ter automata still have the property that at any moment of time, the automaton can be in one state at most. In nondeterministic automata this is not true in general. There are three different ways of formaliz- ing synchronization for these automata. We present a technique able to simulate these formalizations and to give answers to the above problems. The main results of the chapter are Theorem 4.2, Theorem 4.3 and Theorem 4.4 that prove the accuracy of this technique.
In complete deterministic automata the known upper bound of the shortest synchronizing word is cubic in the number of states [23,67,81,82] but on average any random DFA has a synchronizing word which length is much less than this bound (see [43] for experimental results and [64] for their partial theoretical explanation). This fact makes Catalano and Jungers in [14] pose the following open problem:
In nondeterministic automata the upper bound for the length of the short- est synchronizing word is known to be an exponential function in the number of automaton’s states but what about the average length of the shortest synchronizing word in different issues of synchronization?
This problem motivates our experimental research presented in 19

Introduction
Chapter 5. While the random generation of complete deterministic automata is well understood, the random generation of nondeterministic automata is not that obvious. We used two models for the random gener- ation of NFAs. In each model we show how the average length is affected by the parameters of the model. In each model, a series of experiments has been done. Depending on the result of these experiments and using some standard tools of probability theory we give an approximation to the average length of the shortest synchronizing word in different issues of NFAs synchronization.
The main achievements of the thesis
1. A systematic approach to the synchronization problems of partial deterministic and nondeterministic automata based SAT-solver.
2. Proving the validity of presented models from the theoretical point of view and using some benchmarks.
3. Two new series of slowly synchronizing partial deterministic au- tomata.
4. Proving complexity of some problem related to synchronizing non- deterministic automata.
5. Extensive experimental studies of synchronization problems for partial deterministic and nondeterministic automata.
20

Publications
The main results of the dissertation are published in the following papers:
1. Shabana, H., Volkov, M. V.: Using Sat solvers for synchroniza- tion issues in partial deterministic automata. In: Mathematical Optimization Theory and Operations Research, 18th Int. Conf. MOTOR 2019. Communications in Computer and Information Science (CCIS), volume 1090, 103–118. Springer, 2019.
2. Shabana, H.: Exact synchronization in partial deterministic au- tomata. J. Phys.: Conf. Ser., Paper No012047. 1352:1–8, 2019.
3. Shabana, H., Volkov, M. V.: Using Sat solvers for synchronization issues in nondeterministic automata. Siberian Electronic Math. Reports, 15:1426–1442, 2018.
4. Shabana, H.: D2-synchronization in nondeterministic automata. Ural Math. J., 4(2):99–110, 2018.
The first three of these papers are indexed by Scopus, and the third is indexed also by Web of Science.
In the two papers coauthored with the supervisor, the supervisor suggested the general approach while the author developed, justi- fied and implemented all algorithms, designed and performed all experiments, and analyzed experimental results.
In addition, the following computer programs were officially regis- tered at the Russian Federal Service for Intellectual Property:
21
Introduction

Introduction
5. Шабана Ханан Магди Дарвиш. NFAsync: Программный ком- плекс для вычисления порога синхронизации недетерминиро- ванных конечных автоматов. Свидетельство о государственной регистрации программ для ЭВМ No2018663225 от 24 октября 2018. Дата приоритета 26 июня 2018. Правообладатель УрФУ.
6. Шабана Ханан Магди Дарвиш. Программа OSW для вычис- ления оптимального синхронизирующего слова для частичного детерминированного автомата. Свидетельство о государствен- ной регистрации программ для ЭВМ No2019663027 от 08 октяб- ря 2019. Дата приоритета 25 сентября 2019. Правообладатель УрФУ.
Approbation at seminars and conferences
The main results of the dissertation were reported at the following con- ferences and seminars:
1. Seminars of the Department of Algebra and Theoretical Computer Science. Institute of Natural Sciences and Mathematics. Ural Fed- eral University. Yekaterinburg, Russia.
2. International (52-nd) Youth School-Conference of Modern prob- lems in mathematics and its applications, Yekaterinburg, Russia, 2020.
3. InternationalconferenceofMathematicalOptimizationTheoryand Operations Research (MOTOR). Obukhovskoe, Russia, 2019
22

Introduction
4. International Scientific and Practical Conference on Mathemati- cal Modeling, Programming and Applied Mathematics (MMPAM), Veliky Novgorod, Russia 2019.
5. International (51-st) Youth School-Conference of Modern problems in mathematics and its applications, Yekaterinburg, Russia, 2019.
6. International conference (50-th) Youth School-Conference of Mod- ern problems in mathematics and its applications, Yekaterinburg, Russia, 2018.
7. InternationalConferenceandPhD-MasterSummerSchool“Groups and Graphs, Metrics and Manifolds”, Yekaterinburg, Russia, 2017.
Scientific novelty
All results in Chapters 2–5 of the dissertation are new. Chapter 1 collects known results that are used in the thesis. For a few results in Chapter 1, we were not able to locate their proofs in the literature; in such cases, we have provided our proofs for the sake of completeness.
Degree of correctness of the results
All theoretical results presented in the thesis are supplied with rigorous mathematical proofs. The adequacy of experimental results is confirmed by the fact that our results match the ones obtained by other researchers who used alternative approaches.
23

Introduction
Theoretical and practical importance
The dissertation is mainly of theoretical importance. The results ob- tained in it can be used in the theory of finite automata and related areas of theoretical computer science. Computer programs that we developed can serve as prototypes of software products in those information tech- nologies where different types of synchronizing automata are employed.
Research methods
The thesis utilizes methods from various branches of mathematics and theoretical computer science: automata theory, propositional logic, prob- ability theory, graph theory, and complexity theory.
Length and structure of thesis
The thesis consists of an introduction, five chapters, a conclusion, and a bibliography of 91 titles; the total number of pages is 160. The text excludes program codes and datasets, which are available under https://github.com/hananshabana/SynchronizationChecker.
24

Acknowledgments
I would like to thank my supervisor Prof. Dr. Mikhail Volkov for his encouragement, professional guidance, and valuable support during my studies. I wish to thank him for his careful editing that contributed enormously to the production of this thesis.
I would also like to extend my thanks to my colleagues in the De- partment of Algebra and Theoretical Computer Science for their help.
Last, but not least, I would like to thank my husband for his un- derstanding and love during the years of my studies. His support and encouragement were in the end what made this dissertation possible. My parents and brothers receive my deepest gratitude and love for their dedication and kind support.
This work has been supported by a grant from the Egyptian Govern- ment and the Competitiveness Enhancement Program of Ural Federal University, Ekaterinburg, Russia.