The paper illustrates an application of the recently developed method of dealing with controlled automata-based discrete event systems with the help of logical inference. The method based on the calculus of positively constructed formulas is extended on the case of systems built out of sets of modules. Specifications restricting system behavior are also supposed to be modular. Due to the special features of the calculus of positively constructed formulas, it may be applied at the upper level of a robot group control system. The case study of mobile robots pushing a block to a target area is considered.
There are various ways to organize control over a complex technical object. It may be centralized,
decentralized or distributed control. In this paper, one class of systems is in the focus, namely,
the class of Discrete Event Systems (DES), and control implemented by a special object called
supervisor is considered. Supervisory Control Theory (SCT), developed as a tool of restricting
DES behavior according to a set of constraints imposed by some specification, deals with DES
presented in the form of finite state automata as generators of formal languages. A detailed
description of state-of-the-art SCT is presented in, e.g. [
DES for complex systems usually consists, or may be split, into parts, combined using the parallel composition of automata, and there are a set of specifications describing constraints on system functioning, which are relative only to a part of system modules. Modular structures of both DES and specification on DES behavior may be accounted for supervisor constructing and implementing. The main advantage of using modular supervision compared to the monolithic one is a possible saving of memory for storing the supervisor and, in some cases, less computational resources spent for its design.
The modular approach to DES control was studied since 1988 when in [
To intellectualize the solving problems of SCT we suggested the method of dealing with DES
based on the Automated Theorem Proving (ATP) in the calculus of Positively Constructed
Formulas (PCFs). The PCF calculus is a complete method for ATP [
Applying the PCF calculus to SCT for DES, such basic problems as controllability checking [17], supremal controllable sublanguage of a given specification language construction [18] and a monolithic supervisor realization were considered and solved. The developed approach is used to create multi-level hierarchical control systems for mobile robots and robot groups [19]. A small overview of the current state of research on ATP in robotics is presented in [20], while a detailed review on planning in robotics, including the use of ATP, is presented in [21]. The work [22] lies at the intersection of ATP and machine learning, presenting a reinforcement learning toolkit for experiments on guiding ATP in the calculus of connections. The core of the toolkit is a Prolog-based prover. In [23] for planning and control in swarm robotics, the PDDL language is used, which is based on the classical STRIPS-style ATP.
The paper structure is the following. The preliminaries on supervisory control for DES are given in section 2. Section 3 presents the PCF language and the PCF calculus. In section 4, the PCF-based approach to supervisory control is described. In section 5, a case study is given for robot group control using PCFs. The task of moving an object to a target area by a pair of robots is considered. A modular DES and modular specifications are described and modular supervision realizing the specifications are implemented with the help of a PCF. In conclusion, some words on future work are said.
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 [24]. 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 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.
SCT supposes some events of G to be controllable, i.e., they may be prohibited from occurring. Let c be a controllable event set, uc = n c, c \ uc = ;. The means of control G is represented by a supervisor [24]. The supervisor observes events generated by the plant and disables undesired controllable events thus realizing a mapping : L(G) ! 2 c . The supervisor switches control patterns in such a way that the supervised DES achieves a control objective described by some regular language K. The supervisor may be realized, for example, as a pair J = (S; ) where S is a deterministic automaton while : X ! is a function that maps automaton states x, which is a result of a string s 2 L(G) occurring, into control patterns 2 2 . The notion of controllability characterizes languages which may be achieved by the closed-loop structure of the plant and the supervisor. A formal language K is called controllable (with respect to L(G) and uc) if K uc \ L(G) 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. Note that in [17] the method for controllability checking using PCF calculus is presented.
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 [
As a rule, complex technical systems, being subjects of SCT implementation, are composed of smaller subsystems, called modules where each module describes some aspect of system behaviour. Each module may be realised by a generator Gi, i = 1; : : : ; m. To combine modules, the operations of composition of automata are employed, known as product and parallel, or synchronous, compositions. Both operations are essential in supervisor design.
Definition 1 [Parallel composition [
8 ( 1( ; q1); 2( ; q2)) if 1( ; q1)!; 2( ; q2)!; ( ; q1; q2) := <>>>> ( 1( ; q1); q2) iafnd1( ;2q1)!1 a\nd 2; 2 >>>:> (uqn1d;efin2(ed; q2)) otifhe2rw(i;seq2):! and 2 1 n 2; 2 n 1;
Here Ac(G) denotes the operation of taking accessible part of the automaton, that is, deleting all states that are not reachable from q0 by some string of L(G) and transitions attached to these states. Using the same principle, the above definition may be extended on any number of automata. Parallel composition is commutative up to a reordering of the state components in composed states and associative: (G1jjG2)jjG3 = G1jj(G2jjG3). The parallel composition of a set of n automata can therefore be defined using associativity: G1jjG2jjG3 := (G1jjG2)jjG3.
In the parallel composition of two automata events shared by the automata must occur simultaneously thus synchronizing the automata by the common events. Events that are not shared by the automata may occur independently. In SCT parallel composition serves, among other things, to design system model from models of separate modules. If a supervisor is realized with the help of deterministic automaton S then the desired control can be implemented by constructing the parallel composition SjjG of the automata of the plant and the supervisor.
Note that if 1 = 2 then Gi are completely synchronized and the product G1 G2 of automata
G1 and G2 is obtained. If Gi do not share events then they execute events concurrently, and this
case also known as shufle of Gi. In [
There are three paradigms of supervisory control structure nowadays: monolithic, modular, and local modular supervisors. 2.3.1. Monolithic control To built a monolithic supervisor, all generator modules and specifications are composed to a single generator and a single specification. If Ki is a specification language, let Hi be automaton that marks language Ki. Such Hi is called a recognizer of Ki. A monolithic specification is obtained as
Hmono = H1jjH2jj : : : jjHm while monolithic generator is
Gmono = G1jjG2jj : : : jjGn:
Then, if Hmono is controllable then it may be chosen as a monolithic supervisor Smono for Gmono,
and L(J mono=Gmono) = L(SmonojjGmono) [
Gmod = G1jjG2jj : : : jjGn: L(Ji=Gmod) = L(SijjGmod):
Smod = S1jjS2jj : : : jjSm; guarantees that any event of the global plant is enabled only if all modular supervisors that have the corresponding event in their event set enable it.
The benefit of the modular approach is that the desired behavior may be achieved without
constructing the parallel composition of all components. However, then nonblockingness
is considered, the result of modular supervision may appear unsatisfactory, because the
composition of nonblocking supervisors may block. Only nonconflicting languages may be
combined in this case, i.e. such languages L1 and L2 that L1 \ L2 = L1 \ L2. Fortunately,
any two prefix-closed languages are nonconflicting. Moreover, if a language K is prefix-closed
then K"C is prefix-closed as well [
Let each specification Hi has its own generator model Giloc which is the parallel composition of all generator modules Gji that have at least one event in common with Hi: Then, one supervisor Jiloc is designed for each specification:
Giloc = G1jjG2jj : : : jjGnii :
i i
L(Jiloc=Giloc) = L(SilocjjGiloc): Required control as the conjunction of the local supervisors is captured by the parallel composition
Slocmod = S1 jjS2locjj : : : jjSnloc:
loc
In the next sections we will show how modular supervisor can be constructed with the help of the PCF-based approach.
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 (iv) If = fF1; : : : ; Fng is a set of 8-PCFs, then 9X A = 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. is an 9-PCF, is a 8-PCF, 8 9X1 A1 9A5 8B2 8Y3 B4 9X2 A2 9A3 9A4
8Y2 B3
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
8 f9X1 A1 f8Y1 B1; 8B2 f9X2 A2; 9A3 f8Y2 B3g; 9A4gg; 9A5 f8Y3 B4gg can be represented as a tree like in figure 1.
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.
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). 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).
The ATP programming system, a prover, for PCF calculus, called Bootfrost [25], is realized in the Julia programming language as it is aimed mainly at scientific computing and supports JITcompilation (compilation on the fly). It combines such features as high-level development and ease of writing program code, like in Python, and the speed of program execution comparable to programs written in C and Java. Julia has a property of homoiconicity (like Lisp, Clojure or Prolog) that allows one to use program code as data and execute it at the right time. This property is suitable for implementing additional inference strategies. Moreover, it is possible not only to set a strategy in advance but also to generate it dynamically during program execution basing on the state of the logical inference. Since the area of application of the prover is various scientific problems, the wide set of Julia scientific libraries will improve the quality of writing inference strategies for these problems. Multiple dispatching in Julia is well suited for the implementation of symbolic computations, which include the problem of finding inference, due to the elegant and eficient implementation of pattern matching used to solve the matching problem (a special case of unification). Julia also has built-in tools for developing multithreaded and distributed programs.
Figure 2 shows a general form of a PCF representing a DES. It consists of the single base B = fL("; S0); Lm("; S0); (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 where the following predicates are exploited. The predicate L(s; S) denotes “s is a current sequence of events in the state S” and the predicate Lm(s; S) denotes “s is a current sequence of events in the state S, and s is a marked string”. The first arguments of these atoms accumulate the strings of languages generated and marked by the automaton. S0 corresponds to the initial state of the DES. A predicate of the form (S1; ; S2) is interpreted as a transition from a state S1 to a state S2 due to event occurring. If the target state of a transition is marked, then atoms with an index m are used, i.e., m(S1; ; S2). Controlled and uncontrolled events are represented in the base by separate atoms using the predicates c(_) and uc(_), respectively. The function symbol “ ” denotes strings concatenation, and the “"” symbol corresponds to the empty string. 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. 9 B 8 ; s; 0; s0 L( ; s); (s; 0; s0) 8 ; s; 0; s0 L( ; s); m(s; 0; s0) 9L( 9Lm(
The PCF calculus allows one to construct a supremal controllable sublanguage of uncontrollable specification during the controllability checking. The corresponding PCF and the procedure is presented in [18]. Note that one essential feature of the calculus of PCFs is used for sublanguage design, namely, the possibility of constructing a non-monotonic inference by slightly adjusting the definition of the inference rule !. In the non-monotonic inference, atoms may be removed from the base. In general, this operation afects the property of completeness of the PCF calculus but for the problem considered the inference always stops.
The PCF representation of constructing the parallel composition of two automata may also be written using a single PCF. The full PCF, constructing not only automaton G1jjG2 itself but also languages generated by this automaton, are presented in [26]. Here we provide a short version of the PCF from [26] to illustrate automaton structure design using ATP (figure 3). The PCF FG1jjG2 consists of one base subformula which base conjunct BG1jjG2 = f 1(S1i; i; S2i); 2(S1k; k; S2k); 3( ; "; S01S02)g contains atoms for transitions 1, i = 1; n1, of 9 3( ; "; S01S02); 1(S1i; i; S2i); 2(S1k; k; S2k); the automaton G1 and transitions 2, k = 1; n2, of the automaton G2, and also the atom 3( ; "; S01S2) corresponding to the parallel composition automaton. It determines initial state 0 of the composition automaton as combination of the initial states S01, S02 of the automata G1 and G2.
The advantage of the PCF-based method of the parallel composition constructing is that the composition automaton after the completion of the inference does not have inaccessible states, so there is no need to use Ac operation. This is due to control of the connectivity of the graph, representing the automaton, at each step of constructing the inference. It is implemented in PCF with the help of i(_; _; x) atoms where index i is a parameter that takes any of the values f1; 2; 3g.
After the building of the supremal controllable sublanguage of a given specification in the case when the original specification happened to be uncontrollable, this language may be taken as a new specification. Then we can find a solution to the basic problem of supervisory control for a new specification, i.e., a supervisor J such that L(J =G) = K"C . If H0 is a recognizer for K"C then using automata realization of supervisors, a closed-looped behaviour of the plant and the supervisor is realized by the parallel composition of the automata of the plant and the supervisor, i.e., L(J =G) = L(H0jjG).
In PCF formalization, the joint work of the system and the supervisor is carried out using the PCF FSC in figure 4. Here bases B and BS are the sets of atoms corresponding to the transitions 9 B; BS 8 ; s; 0; s0 L( ; s); (s; 0; s0); S(s; 0; s0) 9L( 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 ()), we simultaneously trace the corresponding event in the automaton of the supervisor (an atom S()). The rule works only on those strings that are allowed by the supervisor, i.e., atoms S() limit the answers that could be generated with atoms () 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 control, by applying additional rules to the strings generated. This feature of the PCF calculus may be utilized for optimal supervisory control. The mentioned rules may be defined by an operator. Moreover, the inference can be made interactive, for example, by pausing after each event, or after an event leading the system to the marked state.
Figure 5 shows the general PCF FSmod that represents the work of a generator composed of two modules under supervisory control aimed to guarantee a single specification. Thus, here Gloc = G1jjG2 and one supervisor J loc was previously designed such as to assure L(J loc=Gloc) = L(SlocjjGloc). The base BSloc = BG1 [BG2 [BS [fLE("; E0); Lc("; S0G1 S0G2)g consists of the atoms corresponding to transitions of the automata G1 and G2 (the conjuncts BG1 = f G1(S1; e; S2)g, BG2 = f G2(S1; e; S2)g) and of the automata S (the conjunct BS = f S (S1; e; S2)g) defining specification language. The conjuncts LS ("; S0) and Lc("; S0G1 S0G2) determine initial states for controlled and specification languages generating.
The PCF FSloc is based on the formula for constructing the parallel composition of automata (section 4.2). In contrast to the latter, the questions of FSloc generate strings of the parallel composition of languages, bounded by the supervisor, i.e. by S (S1; e; S2) atoms in the questions. These questions can be interpreted as follows: if a new symbol of the language of the parallel composition of automata may be generated, and at the same time the same symbol can be generated by the automaton of the specification, then construct new strings of these languages accompanied with the states specified in the transitions, and add them to the base.
8 ; 0; s1; s01; s2; s02; s3; s03 Lc( ; s1 s2); G1(s1; 0; s01); G2(s2; 0; s02);
LS ( ; s3); S (s3; 0; s03)
In this section we consider modular supervisor constructing for robot group control. Let on a field, called a scene, there be three robots, two blocks, and the target area to which it is necessary to move the blocks (figure 6). Only a pair of robots can push a block, so at first, a robot should find a companion to form a pair and only then push the block to the target area.
The DES model for the problem under consideration consists of a set of generators, and each of them captures one of the robot actions. The incoming arrow denotes an initial state of an automaton while dotted lines denote controllable events. Marked states are denoted by double circles.
The automaton G1 in figure 7 describes forming of a group of two robots. Event rl is for “companion robot is lost”, rf is for “companion robot is found”. At the state 0, the robot has not yet found a companion, so the event rl does not change the state. Here cG1 = frf g. We set rf to be controllable as the status “companion is found” is determined by external facts. Such notion as composite events may be considered for that [19].
The automaton G2 in figure 8 describes the search of the direction for movement to the block. Events dl is for “direction is lost”, df is for “direction is found”. Again, additional information is used to decide that the right direction is found.
The automaton G3 in figure 9 describes the possible directions of rotation of the robot to find the proper direction of moving. The robot can rotate clockwise and counterclockwise (events cw and ccw). The initial state is north orientation. Both events are controllable. The actual information, whether the direction is found or not, comes from external sources (a deducible event).
The automaton G4 in figure 10 is an automaton that describes the operational modes of robots. The robot can stand still, move, rotate and push. The modes restrict the robot’s functions in diferent situations. For example, when the robot moves or pushes a block, it cannot rotate. Or, until the robot has found a companion, it should not push. This case, for example, is described by a combination of states of automata G1 and G4.
The automaton G5 (figure 11) serves for checking the achievement of the goal assigned, i.e. if the block has reached the target area. The events of G5 are gc – the goal check, ga – the goal is achieved, gna – the goal is not achieved.
cw W cw ccw ccw
N S ccw ccw cw
E cw
The parallel composition of automata G1 G5 represents the current state of the robot. Figure 12 depicts a specification automaton H1. This specification requires that at first, the robot looks 0 dl; rl 0 df 0 rl rf gna gc dl; rl 1
rl dl rl df dl dl 1 cw mv dl
ga mv; ro
pu gna gc 3 4 dl; rl
ga 1 dl 2 df 2 5 2 dl; rl for a partner. Then it finds the right direction, then moves, pushes or rotates, depending on what action is required for the current position of the block. After that, the goal achievement is checked. If the goal is not achieved the actions continue. If the goal has been achieved the task assigned has been solved.
H1. The main strategy.
The specification automaton H2 (figure 13) limits the search for directions. If the direction has not yet been found, then the robot can only rotate clockwise or move.
H2. Finding proper direction.
Consider modular supervisor realization for the modular plant representing robot actions. Note that the specification language L(H) = L(H1jjH2) is controllable. Since checking controllability is not considered in this paper, we omit the proof of this statement. Due to controllability of L(H), it may be taken as a supervisor for the plant G = G1jj : : : jjG5.
According to the local modular control paradigm, we take plant modules G1, G2, G4 G5 and specification H1 to design one supervised subsystem and plant modules G2 and G4, and specification H2 to design another supervised subsystem. Consider the second subsystem. Transitions of automata G2, G4 and H2 are put in the base of the PCF in figure 5. The ifrst question of the resulting formula has no answers because G2 and G4 have no events in common. Answering the second question with the substitution f ! "; 0 ! dl; s1 ! 0; s01 ! 0; s2 ! St; s3 ! 0; s03 ! 1g, we add new atoms Lc(" dl; 0 St); LS (" dl; 1) in the base, which means that the supervisor permitted the transition to the state 1 labeled with the event dl. Next, these atoms are used to find a new answer to the third question: f ! " dl; 0 ! mv; s1 ! 0; s2 ! St; s02 ! M v; s3 ! 1; s03 ! 2g, which gives new atoms L(" dl mv; 0 M v), LS (" dl mv; 2). This means that the supervisor permits the event mv leading to the state 2. And so on, the inference will never end. Table 1 shows the first few steps of the inference found by the prover Bootfrost. It contains the strings of the language L(J2loc=G) extracted from the first arguments of the atoms LS (_; _), and states corresponding to these strings.
The design of the first controlled subsystem may be represented by the PCF in figure 14. This formula is also based on the PCF in figure 5. The base contains atoms corresponding to transitions of generators G1, G2, G4 G5 that have no common events, so the analogue of the first question is not considered as it handles such events only. The second and the third questions, concerning private events, are transformed as shown in the figure.
Overall control assuring both specifications H1 and H2 is achieved by the conjunction of the local supervisors: Slocmod = S1locjjS2loc that is realized with the PCF from section 4.2.
In this paper, the application of the PCF calculus to modular DES control was presented and illustrated with the case study of mobile robots pushing a block to a target area. Realization of the results obtained on the robotic stand is our nearest future work. Further work also supposes solving other SCT problems such as partially observed DES study, design of decentralized supervisors in the automata form, and DES diagnostic. Note that an approach for testing the diagnosability of DES based on a logical representation is proposed in [27]. In contrast to the logical formalism proposed in this paper, [27] uses a less expressive means to represent automata underlying DES: the Conjunctive Normal Form (CNF). DES transitions are described as a set of clauses, which is taken as a new model for DES. Based on the well-known resolution method, an algorithm is presented to test whether failure events can be detected or not for a ifnite number of observable events. A computational comparison of this study with the PCFbased approach proves to be an interesting challenge. Results obtained will be embedded at the diferent levels of the hierarchical control system for mobile robots.
1 0 2
The research was partly supported by the RFBR, project no. 20-07-00397 (section 5), and by the Ministry of Science and Higher Education of the Russian Federation, project no.121032400051-9. [17] Davydov A, Larionov A and Nagul N 2020 2020 43rd International Convention on Information,
Communication and Electronic Technology (MIPRO) pp 1151–1156 [18] Davydov A, Larionov A and Nagul N V 2020 Proceedings of the 2nd International Workshop on Information, Computation, and Control Systems for Distributed Environments, ICCS-DE 2020, Irkutsk, Russia, July 6-7, 2020 (CEUR Workshop Proceedings vol 2638) ed Bychkov I and Tchernykh A (CEUR-WS.org) pp 68–78 [19] Davydov A, Larionov A and Nagul N 2021 J. Phys.: Conf. Series 1864 012048 [20] Davydov A and Larionov A 2020 2020 7th International Conference on Control, Decision and Information
Technologies (CoDIT) vol 1 pp 727–732 [21] Karpas E and Magazzeni D 2020 Annual Review of Control, Robotics, and Autonomous Systems 3 417–439 [22] Zombori Z, Urban J and Brown C E 2020 International Joint Conference on Automated Reasoning (Springer) pp 489–507 [23] Schader M and Luke S 2020 International Conference on Practical Applications of Agents and Multi-Agent
Systems (Springer) pp 224–237 [24] Ramadge P J and Wonham W M 1987 SIAM Journal on Control and Optimization 25 206–230 [25] Pcfbucket 2021 URL http://bootfrost.org [26] Davydov A, Larionov A and Nagul N V 2019 Proceedings of the 1st International Workshop on Information, Computation, and Control Systems for Distributed Environments, ICCS-DE 2019, Irkutsk, Russia, July 8-9, 2019 (CEUR Workshop Proceedings vol 2430) ed Bychkov I and Tchernykh A (CEUR-WS.org) pp 29–41 URL http://ceur-ws.org/Vol-2430/paper3.pdf [27] Geng X, Ouyang D and Han C 2020 Chinese Journal of Electronics 29 304–311