The paper provides a general view on the original logical inference based approach to dealing with discrete event systems as subject to supervisory control theory. The approach proposes a representation of automata-based discrete event system as a positively constructed formula and implementation of the calculus of positively constructed formulas. The stages of a supervisor construction are illustrated with a simplified model of an autonomous underwater vehicle operational modes switching. The supremal controllable sublanguage of the specification and the supervisor are constructed.
The aim of this paper is to give a general view of the logical inference based approach to
dealing with discrete event systems (DES) as subject to supervisory control [
The PCF calculus was presented in [
To illustrate the stages of a supervisor construction procedure, a simplified model of an
autonomous underwater vehicle (AUV) operational modes switching is chosen. As shown in [
The paper is organized as follows. The basic notions of DES and SCT are provided in section 2. The third section contains a brief description of the PCF calculus. In section 4, a way of automata-based DES analysis using PCFs is described. In section 5, a supervised DES is constructed. In conclusion, we discuss some crucial features of the PCF calculus.
Let a discrete event system is specified in the form of a finite-state automata G = (Q; ; ; q0; Qm) as a generator of a formal language [19]. Here Q is the set of states q; is the set of events; : Q ! Q is the transition function; q0 2 Q is the initial state; Qm Q is the set of marked states. G is also called a plant in the automatic control theory. Let = c [ uc, c \ uc = ; where c is a controllable event set. uc = n c. Let denote a Kleene closure, " is an empty string. is easily extended on strings from . Language generated by G is L(G) = fw : w 2 and (w; q0) is defined g, while language marked by G is Lm(G) = fw : w 2 L(G) and (w; q0) 2 Qmg. For any L a closure of L is the set of all strings that are prefixes of words of L, i.e., L = fsjs 2 and 9t 2 : s t 2 Lg. Symbol denotes string concatenation and is often omitted. K is called prefix-closed if K = K.
The Ramadge–Wonham supervisory control framework assumes the existence of a means of control G represented by a supervisor [19]. The supervisor switches control patterns in such a way that the supervised discrete event system achieves a control objective described by some regular language K. A language generated by the closed-looped behavior of the plant and the supervisor is denoted as L(J =G). Let Lm(J =G) denotes the language marked by the supervisor: Lm(J =G) = L(J =G) \ Lm(G). The main goal of supervisory control is to construct such supervisor that L(J =G) = K and Lm(J =G) = K. The definition of controllability characterizes the languages which may be achieved by the closed-loop structure of the plant and the supervisor.
Definition 1 [19] K is controllable (with respect to L(G) and uc) if K uc \ L(G) K.
To verify controllability condition, a product of automata for the system and the specification is built to check if the same uncontrollable transitions present in both the specification and the plant. If the specification under consideration happen to be not controllable, a controllable part of it may be used for designing a supervisor. A set Cin(K) = fL K : L uc \ L(G) Lg is a set of all controllable sublanguages of a given language K [20]. It is well known that since the set of controllable sublanguages of a given regular language L is closed under the union, the supremal controllable sublanguage of L exists, and it is also regular. According [20], we denote this language K"C . Note that in the worst case K"C = ;, while K"C = K if K is controllable.
As a rule, a supervisor is designed as another automaton, and control is implemented by constructing the parallel composition of the automata of the plant and the supervisor. Though the parallel composition of automata can be built using the PCF representation of the automata involved, the supervised DES will be designed in the other way in section 5.
Example 1. Consider a simplified DES model, depicted in figure 1, of autonomous underwater vehicle (i.e., AUV) main operational modes switching while implementing a mission in some underwater area. Here = fm; l; g; r; s; cg with m having the meaning ‘the mission starts’, l ’switch to the loiter mode’, g - ’activate the gathering mode’, r - ’activate the reconfiguration mode’, s - ’surface’, c - ’activate the communication mode’. States of the set Q = fS; M; L; R; Gg correspond to the functioning modes of AUV. Here M (’mission implementation’) is the main mode. G corresponds to the gathering mode which is on when the mission is completed or a corresponding command is received. L is the standby mode: AUV is loitering and waiting for the next orders. R is the reconfiguration mode. S is the mode which corresponds to the start of the mission or surfacing in case of emergency or a command. C is communication mode which supposes a wide-range communication equipment activation for finding other AUVs, a mother ship or command receiving. Let uc = fc; s; rg. All events are observable.
s l C c
L s
S m l m s m g M s g m m r g
G R r
Let the specification language K corresponds to the automaton H in figure 2. K is supposed to be prefix-closed, i.e., K = K. This specification means that communication mode for the AUV is not allowed under any circumstances. This condition may be necessary, for example, if the mission is implemented at a hostile area and the AUV should not be detected by an enemy. Although the model does not pretend to be realistic, it will help us to illustrate the results that follow. It may be noted that such K is not controllable.
Let us consider a language of first-order logic that consists of first-order formulas (FOFs) built out of atomic formulas with &; _; :; !; $ operators, 8 and 9 quantifier symbols and constants true and f alse. The concepts of term, atom, literal we define in the usual way. Hereafter, non-atomic formulas and subformulas will be denoted by capital calligraphic letters (F ; P; Q, etc.), in the general case with indices. Sets of formulas will be denoted by Greek capital letters ( ; , etc.), possibly with indices.
Let X = fx1; : : : ; xkg be a set of variables, A = fA1; : : : ; Amg be a set of atomic formulas called conjunct, and = fF1; : : : ; Fng be a set of FOFs. The following formulas 8x1 : : : 8xk(A1& : : : &Am) ! (F1 _ : : : _ Fn) and 9x1 : : : 9xk(A1& : : : &Am)&(F1& : : : &Fn) are denoted as 8x1; : : : ; xkA1; : : : ; AmfF1; : : : ; Fng and 9x1; : : : ; xkA1; : : : ; AmfF1; : : : ; Fng. They can be abbreviated as 8X A and 9X A respectively, keeping in mind that the 8-quantifier corresponds to ! _, where _ means disjunction of all the formulas from , and 9-quantifier corresponds to & &, where & means conjunction of all the formulas from . Any of sets X, A, may be empty, and in this case they could be omitted in formulas. Thus, if Q 2 f8; 9g then QX A ? QX A, QX ? QX and Q?A QA . Since empty disjunction is identical to f alse, whereas empty conjunction is identical to true, the following equivalences are correct: 8X A ? 8X A ! f alse 8X A and 9X A ? 9X A&true 9X A and 8? true ! 8 and 9? true& 9 .
Definition 2 . Let X be a set of variables, and A be a conjunct, both can be empty. (i) 9X A is an 9-PCF, (ii) 8X A is a 8-PCF, (iii) If = fF1; : : : ; Fng is a set of 8-PCFs, then 9X A (iv) If = fF1; : : : ; Fng is a set of 9-PCFs, then 8X A (v) Any 9-PCF or 8-PCF is a PCF, (vi) There are only PCFs of a form 9-PCF and 8-PCF.
The term “positively” comes from the fact that according to definition 3 PCFs contain no negation operator :.
For the sake of readability, we represent PCFs as trees whose nodes are type quantifiers, and we use corresponding notions: node, root, leaf, branch. For example, a PCF is represented as a tree as follows: 8 9X1 A1
Given PCFs P = 8fF1; : : : ; Fng and Fi = 9Xi BifQi1; : : : ; Qimg, i = 1; n, then Fi is called base subformula of P, Bi is called base of facts or just base, Qij are called question subformulas, and roots of question subformulas are called questions to the base Bi, i = 1; n. A question of a form 8X A (without any children) is called goal question.
Inside each of the base subformulas, any variable cannot be free and bound simultaneously. Furthermore, it cannot be bound by diferent quantifiers simultaneously.
Example 2. The general form of PCF representing some automaton consists of the single base B = fI(S); L("; S); Lm("; S); (S1i; i; S2i); m(S1i; i; S2i); c( j ); uc( j )g, i 2 f1; : : : ; ng, j 2 f1; : : : ; kg, n is the number of transitions, k is the number of events, and two questions shown in figure 3. Here L(s; S) denotes “s is a current sequence of events in the state S” and Lm(s; S) denote “s is a current sequence of events in the state S, and s is a marked string”. The first arguments of these atoms will accumulate the strings of languages generated and marked by the automaton. Predicate of the form (S1; ; S2) will be interpreted as the automaton transition from a state S1 to a state S2 with an event . If the target state of a transition is marked, then delta atoms with an index m are used, i.e., m(S1; ; S2) if S2 is a marked state. The predicate I(_) denotes the initial state of the automaton. Controlled and uncontrolled events will be represented in the base by separate atoms using the predicates c(_) and uc(_), respectively. As usual, the function symbol “ ” denotes strings concatenation, and the “"” symbol corresponds to the empty string.
Definition 3. [Answer] Consider some base subformula 9X A of a PCF. A question of the subformula Q = 8Y B , Q 2 has an answer if and only if is a substitution Y ! H1 [ X and B A, where H1 is Herbrand universe based on constant and function symbols that occur in the corresponding base subformula.
Definition 4. Let P1 = 9X A and P2 = 9Y B , then merge(P1; P2) = 9X[Y A [ B [ .
Definition 5. Consider some base subformula B = 9X A . A question subformula Q 2 has the form 8Y D fP1; : : : ; Png, where Pi = 9Zi Ci i; i = 1; n, then split(B; Q) = fmerge(B; P10); : : : ; merge(B; Pn0)g, where 0 is a variable renaming operator. We say that B is split by Q, and split(B; Q) is the result of the split of B. Obviously, split(B; 8Y D) = ?.
Definition 6. [The inference rule !] Consider some PCF F = 8 . If there exists a base subformula B = 9X A , B 2 and there exists a question subformula Q 2 , and the question of Q has an answer to B, then !(F ) = 8 n fBg [ split(B; Q ):
Note, that if the set becomes empty after applying the ! rule, and the PCF becomes just 8, then the negation of the original statement is unsatisfiable; therefore, the statement itself is true.
Any finite sequence of PCFs F ; !F ; !2F ; : : : ; !nF , where !sF = !(!s 1F ); !1 = !; !nF = 8, is called an inference of F in the PCF calculus (with the axiom 8).
Suppose that a search strategy used by default does not use repeated application of ! to a question with the same (question-answering method of automated inference search).
Example 3. The generator G depicted in figure 1 may be represented by the PCF shown in ifgure 3 with B being the conjunct fI1(L); L("; L); uc(c); 1(S; r; M ); 1(M; s; S); 1(M; l; L); 1(M; g; G); 1(M; r; R); 1(L; s; S); 1(L; c; C); 1(L; m; M ); 1(L; g; G); 1(G; r; R); 1(G; m; M ); 1(R; s; S); 1(R; g; G); 1(R; m; M ); 1(C; l; L); 1(C; m; M ); 1(C; s; S); 1m(L; s; S); 1m(C; s; S); 1m(M; s; S); 1m(R; s; S)g: Applying the inference rules to this PCF, the words of the languages generated and marked by the automaton are constructed as the first arguments of the atoms L(s; S), Lm(s; S) in the base.
One of the essential features of the calculus of PCFs which will be used later is that we can build a non-monotonic inference by only slightly adjusting the definition of the inference rule. For this, we introduce the operator , which will mark the atoms in the questions. Now, if a question with atoms marked with the operator has an answer, then after applying the inference rule, the atoms in the base that participated in the matching search with the marked atoms should be removed from the base. In general, the operator afects the property of completeness of the PCF calculus, but for the problem considered in this paper, thanks to a proper formalization, the inference using always stops. 4. Supremal controllable sublanguage construction using a PCF inference 4.1. Product of automata construction Suppose that behaviour of G should be constrained within the specification language K, and let automaton H generates, or recognizes, K. Before deigning a supervisor, the controllability of K must be verified by comparing uncontrollable transitions in automata G and H. To merge the corresponding states of the automata, a product of G and H is built. The PCF FG H (figure 4) constructing the product of automata consists of one base subformula, which base conjunct is BG H = fI1(S0); I2(P0); 1(S1i; i; S2i); 2(S1k; k; S2k)g, containing atoms for transitions 1, i = 1; n1, of the automaton G and transitions 2, k = 1; n2, of the automaton H. 9 BG H 8s; p I1(s); I2(p) 8s; p I1(s); I2(p) 8 ; s1; p1; s2; p2; 0; s0 1(s1; ; s2);
2(p1; ; p2); 3(s0; 0; s1 p1) 9I3(s p) 9 3(
; "; s p) 9 3(s1 p1; ; s2 p2)
Index one in the subscripts of atoms of this formula corresponds to the atoms of the automaton G, two corresponds to the H, and three corresponds to the atoms of G H. Here, the functional symbol is used to trace the pairs of states in the product automaton. The first question adds the initial state of the product automaton to the base. The second question adds an undetermined transition atom corresponding to the third automaton, thanks to which the connectivity of the product automaton is controlled in the third question. The latter adds the transition atoms of the product automaton to the base.
Example 4. figure 5 shows the product of the automaton G shown in figure 1 with the automaton H shown in figure 2. S,1 l m s m
g M,2
s 9 BC g m m
r Q1 Q2 : : : Q6 R,5
r
To check controllability, we use PCF FC with the base BC = BG H [ f 3(S1k1 S2k1; k; S1k2 S2k2)g, k = 1; n3, that contains predicate descriptions of states and transitions of G, H, and recently added transitions of the function 3 of G H. Let the questions to the base of FC be as depicted in figure 6. The questions have the following meaning.
Q2 : 8s1; s2; p1; Q3 : 8p1; p2; Q4 : 8p1; Q5 : 8p1; Q6 : 8s1; s2; p1; p2;
Chk(p1; ; 0)
U C(p1; ) Q1 : 8s1; s2; p1; p2; I1(s1); I3(p1); 1(s1; ; s2); 3(p1; ; p2) 9 N (s1; p1) N (s1; p1); 1(s1; ; s2); Euc( )
9 Chk(p1; ; 0) Chk (p1; ; 0); 3(p1; ; p2)
9 Chk(p1; ; 1) 9 U C(p1; ) N (s1; p1); 1(s1; ; s2); 3(p1; ; p2)
9 N (s2; p2):
Q1 adds to the base the initial states of G and G H as the first pair of states to be checked for violating controllability. We call states which are simultaneously achieved from the states of G and G H by the same event the neighbouring states. The predicate N (_; _) is used to store pairs of neighbouring states. Initial states of G and G H are not neighbouring in our sense, but N (s1; p1) with them is necessary for further inference.
Q2 adds to the base the atom Chk(p1; ; 0) which means that there is an uncontrollable transition from the state p1 of the automaton G. If there is no such transition from the state p1 of H, K is not controllable. This is checked by the next rule.
Q3 checks if both neighbouring states share the same uncontrollable event. A successful answer to this question means that the uncontrollable event is legal, i.e., allowed by the specification, since a transition labelled by it exists in both G and H. In this case, the atom Chk(p1; ; 0) is deleted from the base with the help of operator.
Q4 checks if the atom Chk(p1; ; 0) is present in the base. Such atom contains information about the state p1 and the event that violate the controllability condition.
Q5 is the goal question that ends the inference.
Q6 adds the next pair of states to be checked to continue the inference search.
Since the formalized automata are finite with the finite sets of events, then the search space for the inference in this formalization is finite. If the inference has finished with the exhaustion of the search options for substitutions and the answer to the goal question has not been found, then the specification language is controllable.
Example 5. It may be noted that the specification in figure 2 is not controllable due to the event e at the state L. We do not provide here the inference proving it but leave this issue till the next subsection.
Slightly changing questions of the PCF FC , we can construct K"C during the checking controllability of K. Consider the PCF FS depicted in figure 7. Let questions Q1S – Q3S are the same as the questions Q1 – Q3 of the PCF FC above and have the same interpretation, Q5S coincides with Q6. The rest of the questions are interpreted as follows.
9 BS
Q1S Q2S : : : Q7S Q4S : 8p1; Chk(p1; ; 0)
9 Del(p1) Q5S : 8s1; s2; p1; p2; N (s1; p1); 1(s1; ; s2); 3(p1; ; p2) 9 N (s2; p2) Q6S : 8p11; p12; p21; p22; Del(p11 p12); 2(p12; ; p22); 3(p11 p12; ; p21 p22) Q7S : 8p11; p12; p21; p22; Del(p21 p22); 2(p12; ; p22); 3(p11 p12; ; p21 p22) 9 Deleted(p12; ; p22) 9 Deleted(p12; ; p22)
As Q4 does, Q4S checks if the atom Chk(p1; ; 0) is present in the base and, additionally, marks the state p1 for deletion with the help of the predicate Del(_). The atom Del(p1) is further used in questions Q6S, Q7S to delete transitions associated with the state p1. The rules Q6S, Q7S are simple and straightforward. If the Del(p1) atom was added to the base, then state p1 should be deleted from the automaton H. Thus, Q6S removes all transitions leaving this state and Q7S removes all transitions leading to this state.
To construct a supremal controllable sublanguage of K, we use the following strategy. The inference is built by checking the applicability of the inference rule to questions in order from Q1S to Q7S. The rules Q1S – Q5S check whether the specification is controllable or not. The rules Q6S, Q7S remove transitions associated with the state in which an event occurs that violates the controllability condition. If during the application of the Q1S – Q5S rules the answer to question Q4S was found, an atom Del(_) denoting uncontrollability of K is added to the base. Then we apply the rules Q6S, Q7S, ignoring the rules from the Q1S – Q5S, until possible substitutions for applying the inference rule to Q6S and Q7S are not exhausted. Next, the process is repeated until the inference stops, having exhausted all possible substitutions. Thus, if for the given specification a controllable sublanguage is empty, then during the inference all transitions of the automata corresponding to the specification will be deleted. Consider this strategy with an example.
Example 6. Table 1 shows the inference of the PCF, which constructs the supremal controllable sublanguage of the specification K represented by the automaton shown in figure 2. It is assumed that the product automaton (figure 5) is already built, and the base from which the inference starts includes the next subset of atoms: fI1(S); I3(S 1); uc(c); uc(r); uc(s); 1(S; r; M ); 1(M; s; S); 1(M; l; L); 1(M; g; G); 1(M; r; R); 1(L; s; S); 1(L; c; C); 1(L; m; M ); 1(L; g; G); 1(G; r; R); 1(G; m; M ); 1(R; s; S); 1(R; g; G); 1(R; m; M ); 1(C; l; L); 1(C; m; M ); 1(C; s; S); 2(S; r; M ); 2(M; s; S); 2(M; l; L); 2(M; g; G); 2(M; r; R); 2(L; m; M ); 2(L; g; G); 2(G; r; R); 2(L; s; S); 2(G; m; M ); 2(R; s; S); 2(R; g; G); 2(R; m; M ); 3(S 1); m; M 2); 3(M 2); s; S 1); 3(M 2); l; L 3); 3(M 2); g; G 4); 3(M 2); r; R 5); 3(L 3); s; S 1); 3(L 3); m; M 2); 3(L 3); g; G 4); 3(G 4); r; R 5); 3(G 4); m; M 2); 3(R 5); s; S 1); 3(R 5); g; G 4); 3(R 5); m; M 2)g For convenience, in the table, we omit the superscript S in questions names. The automaton recognizing K"C is shown in figure 8.
X1 m s
X2 s g m m r
X4 g X5 r Q Base atoms used Step Result 12 N (R; R 5); Another check is assigned Q2 1(R; s; S) for the event s which may uc(s) occur at the state R 13 Chk(L 3; s; 0) fp1 ! L 3; Chk(L 3; s; 1) The check assigned at the Q3 (deleted); p2 ! S 1; step 10 is passed, i.e., viola3(L 3; s; S 1) ! sg tion of controllability is not found 14 Chk(G 4; r; 0) fp1 ! G 4; Chk(G 4; r; 1) The check assigned in the Q3 (deleted); p2 ! R 5; step 11 is passed, i.e., viola3(G 4; r; R 5) ! rg tion of controllability is not found 15 Chk(R 5; s; 0) fp1 ! R 5; Chk(R 5; s; 1) The check assigned at the Q3 (deleted); p2 ! S 1; step 12 is passed, i.e., viola3(R 5; s; S 1) ! sg tion of controllability is not found 16 N (L; L 3); fs1 ! L; s2 ! C; Chk(L 3; c; 0) The same as at the previous Q2 1(L; c; C) p1 ! L 3; ! cg step, the check assigned uc(c) for another uncontrollable transition from L labeled with c 17 Chk(L 3; c; 0) fp1 ! L 3; Del(L 3; c) The check assigned at the Q4 ! cg previous step was failed; therefore, the specification corresponding to the automaton H is uncontrollable.
Since the tested specification is uncontrollable, the rules for deleting the transitions associated with the state found in the previous steps are triggered.
Base atoms used 20 Del(L 3); Q6 2(3; m; 2); 3(L 3; m; M 2) fp11 ! L; p12 ! 3; p21 ! M; p22 ! 2; ! mg 21 Del(L 3); Q7 2(2; l; 3); 3(M 2; l; L 3) fp11 ! M; p12 ! 2; p21 ! L; p22 ! 3; ! lg
Deleted(3; m; 2) Deleted(2; l; 3)
In the previous section, we have considered the way of building the supremal controllable sublanguage for the given specification. Taking this language as a new specification, we can ifnd a solution of the basic problem of supervisory control, i.e., a supervisor J and the closedlooped system such that L(J =G) = K"C . A closed-looped behaviour of the plant and the supervisor is usually realized by the parallel composition of the corresponding automata of the plant and the supervisor, i.e., L(J =G) = L(J jjG) [20]. In our formalization, the joint work of the system and the supervisor is carried out using the PCF FSC below.
9 B; BS 8 ; s; 0; s0 L( ; s); 1(s; 0; s0); 2(s; 0; s0) 9L(
Here bases B and BS are the sets of atoms corresponding to the transitions of the plant and the supervisor, correspondingly. The only question of FSC may be interpreted as follows. If the system is at the state s and an event occurs, then according to the 2, the system is switched to the specified state s0, and is added to the current chain of events stored as the first argument of the predicate L(_; _). That is, for any transition corresponding to the language L(G) (an atom 1()), we simultaneously trace the corresponding event in the automaton of the supervisor (an atom 2()). The rule works only on those strings that are allowed by the supervisor, i.e., atoms 2() limit the answers that could be generated with atoms 1() only.
Note that the inference is organized in such a way as to assure a sequential accumulation of events. This means that, first of all, all possible continuations from the initial state will be added to the empty string. After then, all events from the neighbouring states will be added to all strings of the length one in the base, and so on. The search strategy can also be configured to analyze strings. For example, when all strings of a given length are generated, each next transition can be controlled in addition to the supervisor, by applying additional rules on the appeared strings. This feature of the PCF calculus may be utilized for the optimal supervisory control. The mentioned rules may be defined by an operator. Moreover, all the inference can be made interactive, for example, by pausing after each event, or after an event leading the system to the marked state.
Example 7. Table 2 demonstrates the fist steps of the inference generating L(J =G) for the AUV model from the Example 1. Taking the language recognized by the automaton HK"C in ifgure 8 as a new specification, we build the closed-looped system such that L(J =G) = K"C using the PCF FSC with B being the set of atoms corresponding to the transitions of G and BS being the set of atoms corresponding to the transitions of HK"C : fL("; X1); uc(c); uc(r); uc(s); 2(X1; m; X2); 2(X2; s; X1); 2(X2; g; X4); 2(X2; r; X5); 2(X4; r; X5); 2(X4; m; X2); 2(X5; s; X1); 2(X5; g; X4); 2(X5; m; X2); 2(C; m; X2); 2(C; s; X1); 2m(C; s; X1); 2m(X2; s; X1); 2m(X5; s; X1)g
In this paper, we intended to provide a full picture on the PCF calculus based approach to solving some basic problems of SCT for DES in the automata form. The formalization of DES as PCF is presented and algorithms for controllability checking and the supremal controllable sublanguage construction are illustrated.
A few words must be said about the end of the work of the inference search machine for the PCFs exploited above. In the classical variant of the PCF calculus, there are three possible results of the search for an inference of some formula F :
1) the inference of F is constructed, i.e., according to the definition, all base subformulas have been refuted, so F is proved to be unsatisfiable;
2) the inference of F is not constructed, but the inference search machine has stopped, having exhausted all variants of substitutions for the application of the inference rule; in this case, we may speak about the completed proof of satisfiability of F ;
3) the inference of F is not constructed and the inference search machine has stopped without exhausting all the substitution variants for applying the inference rule, i.e., stopped by the forced shutdown; in this case, nothing can be said about the satisfiability of F .
When considering a particular PCF in this article, we stipulate which of the options for completing the inference we mean when applying the inference search machine to this formula. The exception is the last formula. This formula simulates the generation of a possibly infinite formal language, and therefore it is constructed in such a way that its inference does not end.
The further work supposes modular and partially observed DES study, design of decentralized supervisors, and temporal logic implementation for SCT via the PCF calculus. Results obtained will be embedded at the diferent levels of the hierarchical control system for mobile robots.
The research was partly supported by the RFBR, project no. 20-07-00397 (sections 2 and 5), and by the Basic Research Program of SB RAS, project no. IV.38.1.1. [15] Hill R C and Lafortune S 2017 2017 American Control Conference (ACC) pp 3840–3847 ISSN 2378-5861 [16] Gamage G W, Mann G K I and Gosine R G 2009 Proceedings of the 2009 IEEE RSJ International Conference on Intelligent Robots and Systems IROS 09 (Piscataway, NJ, USA: IEEE Press) pp 4831–4836 ISBN 9781-4244-3803-7 [17] Lopes Y K, Trenkwalder S M, Leal A B, Dodd T J and Groß R 2016 Swarm Intelligence 10 65–97 ISSN 1935-3820 [18] Mendiburu F J, Morais M R A and Lima A 2016 IEEE International Conference on Automatica (ICA-ACCA)
Oct. 2016 1 – 7 ISSN 2405-8963 [19] Ramadge P J and Wonham W M 1987 SIAM Journal on Control and Optimization 25 206–230 [20] Cassandras C G and Lafortune S 2008 Introduction to Discrete Event Systems (Springer US)