Logic inference based construction of a supervisor for a discrete event system Artem Davydov, Aleksandr Larionov and Nadezhda Nagul Matrosov Institute for System Dynamics and Control Theory of the Siberian Branch of the Russian Academy of Sciences, 134 Lermontov str., 664033 Irkutsk, Russia E-mail: artem@icc.ru, bootfrost@zoho.com, sapling@icc.ru Abstract. 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. 1. Introduction 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 [1]. The approach proposes a representation of automata-based DES as a positively constructed formula (PCF), and implementation the PCF calculus for proving it. During the inference, languages generated and marked by DES as a generator of formal languages are obtained. Thus, automata are simulated. The same technique is used to construct parallel composition and product of automata. These structures are then applied for supervisory control theory (SCT) basic problems solving. The approach was developed in authors’ several works [2, 3, 4] that concerned DES formalization, controllability, observability and coobservability of specifications on DES functioning checking, and supervisor implementation. To provide the main ideas of the method and algorithms involved, many technical details were omitted in those papers due to the space limitations. This paper fills in the blanks which might remain. The PCF calculus was presented in [5, 6] and further developed in [7]. Due to its features, the PCF calculus allows one to combine the automatic search for logic inferences with special domain-based heuristics which are customizable for a task being solved. Moreover, modifiability of semantics, which may be constructive, non-monotonic or temporal, and an ability to construct intuitionistic inferences of some non-Horn formulas, are helpful at solving problems of dynamic systems control. Problems of automated theorem proving software in the PCF calculus design and implementation are briefly discussed in [8]. 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 [9] Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). and [10], both the PCF calculus and DES may be employed at the various levels of a hierarchical control system for AUV and AUVs groups. Indeed, SCT is actively utilized in robotics nowadays. Recent publications in this area concern single robot control [11], [12], robot groups control [13], [14], [15], robots formation control [16], and swarm robotics [17], [18]. On the other hand, the inference search machines, implemented at a robot control system, are applied to represent and process the knowledge obtained during the robot functioning. Constructive semantics of the PCF calculus allows one to extract the knowledge (for example, AUV action plans) from inferences, while non-monotonicity and time tracking help to construct plans in dynamically changing subject areas. Interactive properties of the PCF calculus, its application for dynamic systems control and action planning are described in [6] with the examples of elevator group control, mobile robot action planning and telescope guidance. Application of PCFs based ATP and logical inference, embedded at the upper level of the control system, to DES at the middle level allows efficiently solving control problems emerging during the performance of the robot’s mission. 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. 2. Supervisory control of DES 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 ∈ 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 = Σ \ Σc . Let Σ∗ denote a Kleene closure, ε is an empty string. δ is easily extended on strings from Σ∗ . Language generated by G is L(G) = {w : w ∈ Σ∗ and δ(w, q0 ) is defined}, while language marked by G is Lm (G) = {w : w ∈ L(G) and δ(w, q0 ) ∈ Qm }. For any L ⊂ Σ∗ a closure of L is the set of all strings that are prefixes of words of L, i.e., L = {s|s ∈ Σ∗ and ∃t ∈ Σ∗ : s · t ∈ L}. 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) = {L ⊆ K : LΣuc ∩ L(G) ⊆ L} 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 Σ = {m, l, g, r, s, c} 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 = {S, M, L, R, G} 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 = {c, s, r}. All events are observable. g L G l m g c l m r s C m M g s r m m s S s R Figure 1. Generator of the language for the plant G. 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. 3. Representation of DES in the calculus of PCFs Let us consider a language of first-order logic that consists of first-order formulas (FOFs) built out of atomic formulas with &, ∨, ¬, →, ↔ operators, ∀ and ∃ 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 = {x1 , . . . , xk } be a set of variables, A = {A1 , . . . , Am } be a set of atomic formulas called conjunct, and Φ = {F1 , . . . , Fn } be a set of FOFs. The following formulas ∀x1 . . . ∀xk (A1 & . . . &Am ) → (F1 ∨ . . . ∨ Fn ) and ∃x1 . . . ∃xk (A1 & . . . &Am )&(F1 & . . . &Fn ) are g 2 4 m g l m r s 2 g r m m s 1 s 5 Figure 2. Recognizer H for the specification K. denoted as ∀x1 , . . . , xk A1 , . . . , Am {F1 , . . . , Fn } and ∃x1 , . . . , xk A1 , . . . , Am {F1 , . . . , Fn }. They can be abbreviated as ∀X A Φ and ∃X A Φ respectively, keeping in mind that the ∀-quantifier corresponds to → Φ∨ , where Φ∨ means disjunction of all the formulas from Φ, and ∃-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 ∈ {∀, ∃} 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: ∀X A ∅ ≡ ∀X A → f alse ≡ ∀X A and ∃X A ∅ ≡ ∃X A&true ≡ ∃X A and ∀∅ Φ ≡ true → Φ ≡ ∀ Φ and ∃∅ Φ ≡ true&Φ ≡ ∃ Φ. Definition 2. Let X be a set of variables, and A be a conjunct, both can be empty. (i) ∃X A is an ∃-PCF, (ii) ∀X A is a ∀-PCF, (iii) If Φ = {F1 , . . . , Fn } is a set of ∀-PCFs, then ∃X A Φ is an ∃-PCF, (iv) If Φ = {F1 , . . . , Fn } is a set of ∃-PCFs, then ∀X A Φ is a ∀-PCF, (v) Any ∃-PCF or ∀-PCF is a PCF, (vi) There are only PCFs of a form ∃-PCF and ∀-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 ∀ {∃X1 A1 {∀Y1 B1 , ∀B2 {∃X2 A2 , ∃A3 {∀Y2 B3 }, ∃A4 }}, ∃A5 {∀Y3 B4 }} is represented as a tree as follows: ∀Y1 B1 ∃X1 A1 ∃X2 A2 ∀B2 ∃A3 ∀Y2 B3 ∀ ∃A4 ∃A5 ∀Y3 B4 Given PCFs P = ∀{F1 , . . . , Fn } and Fi = ∃Xi Bi {Qi1 , . . . , Qim }, 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 ∀X 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 different quantifiers simultaneously. Example 2. The general form of PCF representing some automaton consists of the single base B = {I(S), L(ε, S), Lm (ε, S), δ(S1i , σ i , S2i ), δ m (S1i , σ i , S2i ), Σc (σ j ), Σuc (σ j )}, i ∈ {1, . . . , n}, j ∈ {1, . . . , k}, 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) ∀σ, s, σ 0 , s0 L(σ, s), δ(s, σ 0 , s0 ) ∃L(σ · σ 0 , s0 ) ∃B ∀σ, s, σ 0 , s0 L(σ, s), δ m (s, σ 0 , s0 ) ∃Lm (σ · σ 0 , s0 ) Figure 3. General form of PCF representation of an automaton. 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 ∃X A Ψ of a PCF. A question of the subformula Q = ∀Y B Φ, Q ∈ Ψ has an answer θ if and only if θ is a substitution Y → H ∞ ∪ X and Bθ ⊆ A, where H ∞ is Herbrand universe based on constant and function symbols that occur in the corresponding base subformula. Definition 4. Let P1 = ∃X A Ψ and P2 = ∃Y B Φ, then merge(P1 , P2 ) = ∃X∪Y A ∪ B Ψ ∪ Φ. Definition 5. Consider some base subformula B = ∃X A Ψ. A question subformula Q ∈ Ψ has the form ∀Y D {P1 , . . . , Pn }, where Pi = ∃Zi Ci Γi , i = 1, n, then split(B, Q) = {merge(B, P10 ), . . . , merge(B, Pn0 )}, 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, ∀Y D) = ∅. Definition 6. [The inference rule ω] Consider some PCF F = ∀ Φ. If there exists a base subformula B = ∃X A Ψ, B ∈ Φ and there exists a question subformula Q ∈ Ψ, and the question of Q has an answer θ to B, then ω(F) = ∀ Φ \ {B} ∪ split(B, Qθ). Note, that if the set Φ becomes empty after applying the ω rule, and the PCF becomes just ∀, then the negation of the original statement is unsatisfiable; therefore, the statement itself is true. Any finite sequence of PCFs F, ωF, ω 2 F, . . . , ω n F, where ω s F = ω(ω s−1 F), ω 1 = ω, ω n F = ∀, is called an inference of F in the PCF calculus (with the axiom ∀). 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 figure 3 with B being the conjunct {I1 (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)}. 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 ∗ affects 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 = {I1 (S0 ), I2 (P0 ), δ1 (S1i , σ i , S2i ), δ2 (S1k , σ k , S2k )}, containing atoms for transitions δ1 , i = 1, n1 , of the automaton G and transitions δ2 , k = 1, n2 , of the automaton H. ∀s, p I1 (s), I2 (p) ∃I3 (s · p) ∀s, p I1 (s), I2 (p) ∃δ3 (ξ · ρ, ε, s · p) ∃ BG×H ∀σ, s1 , p1 , s2 , p2 , σ 0 , s0 δ1 (s1 , σ, s2 ), δ2 (p1 , σ, p2 ), ∃δ3 (s1 · p1 , σ, s2 · p2 ) δ3 (s0 , σ 0 , s1 · p1 ) Figure 4. PCF constructing the product of automata. 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. g L,2 G,4 m g l m r s M,2 g r m m s S,1 R,5 s Figure 5. The product of G and H. 4.2. Controllability checking To check controllability, we use PCF FC with the base BC = BG×H ∪ {δ3 (S11 k · S k , σ k , S k · S k )}, 21 12 22 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. Q1 Q2 ∃ BC ... Q6 Q1 : ∀s1 , s2 , p1 , p2 , σ I1 (s1 ), I3 (p1 ), δ1 (s1 , σ, s2 ), δ3 (p1 , σ, p2 ) − ∃ N (s1 , p1 ) Q2 : ∀s1 , s2 , p1 , σ N (s1 , p1 ), δ1 (s1 , σ, s2 ), Euc (σ) − ∃ Chk(p1 , σ, 0) Q3 : ∀p1 , p2 , σ Chk ∗ (p1 , σ, 0), δ3 (p1 , σ, p2 ) − ∃ Chk(p1 , σ, 1) Q4 : ∀p1 , σ Chk(p1 , σ, 0) − ∃ U C(p1 , σ) Q5 : ∀p1 , σ U C(p1 , σ) Q6 : ∀s1 , s2 , p1 , p2 , σ N (s1 , p1 ), δ1 (s1 , σ, s2 ), δ3 (p1 , σ, p2 ) − ∃ N (s2 , p2 ). Figure 6. PCF FC for controllability checking. 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. 4.3. Controllable sublanguage construction 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 QS1 – QS3 are the same as the questions Q1 – Q3 of the PCF FC above and have the same interpretation, QS5 coincides with Q6 . The rest of the questions are interpreted as follows. QS1 ∃ BS QS2 ... QS7 QS4 : ∀p1 , σ Chk(p1 , σ, 0) − ∃ Del(p1 ) QS5 : ∀s1 , s2 , p1 , p2 , σ N (s1 , p1 ), δ1 (s1 , σ, s2 ), δ3 (p1 , σ, p2 ) − ∃ N (s2 , p2 ) QS6 : ∀p11 , p12 , p21 , p22 , σ Del(p11 · p12 ), δ2∗ (p12 , σ, p22 ), δ3∗ (p11 · p12 , σ, p21 · p22 )− − ∃ Deleted(p12 , σ, p22 ) QS7 : ∀p11 , p12 , p21 , p22 , σ Del(p21 · p22 ), δ2∗ (p12 , σ, p22 ), δ3∗ (p11 · p12 , σ, p21 · p22 )− − ∃ Deleted(p12 , σ, p22 ) Figure 7. PCF FS for controllable sublanguage construction. As Q4 does, QS4 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 QS6 , QS7 to delete transitions associated with the state p1 . The rules QS6 , QS7 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, QS6 removes all transitions leaving this state and QS7 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 QS1 to QS7 . The rules QS1 – QS5 check whether the specification is controllable or not. The rules QS6 , QS7 remove transitions associated with the state in which an event occurs that violates the controllability condition. If during the application of the QS1 – QS5 rules the answer to question QS4 was found, an atom Del(_) denoting uncontrollability of K is added to the base. Then we apply the rules QS6 , QS7 , ignoring the rules from the QS1 – QS5 , until possible substitutions for applying the inference rule to QS6 and QS7 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: {I1 (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)} For convenience, in the table, we omit the superscript S in questions names. The automaton recognizing K ↑C is shown in figure 8. X4 g m r X2 g r m m s X1 X5 s Figure 8. Recognizer for the supremal controllable sublanguage of K. Table 1. Constructive inference building the supremal controllable sublanguage of the specification. Q Base atoms used Substitution Atoms added Step Result 1 I1 (S), I3 (S · 1), {s1 → S, s2 → M, N (S, S · 1) The pair of states S and Q1 δ1 (S, m, M ), p1 → S · 1, p2 → (S, 1) in the automata G and δ3 (S ·1, m, M ·2) M · 2, G × H is to be checked for σ → m} violation of controllability 2 N (S, S · 1), {s1 → S, s2 → M, N (M, M · 2) The same as at the first step Q5 δ1 (S, m, M ), p1 → S · 1, p2 → of this inference δ3 (S ·1, m, M ·2) M · 2, σ → m} 3 N (M, M · 2), {s1 → A, s2 → C, Chk(M · 2, s, 0) In automaton G an uncon- Q2 δ1 (M, s, S) p1 → A · 1, σ → a} trolled transition labeled by Σuc (s) the event s was found, i.e., the check of the correspond- ing transition in the au- tomaton G × H is necessary 4 N (M, M · 2), {s1 → M, s2 → R, Chk(M · 2, r, 0) The same as in previous Q2 δ1 (M, r, R) p1 → M · 2, σ → a} step, the check assigned for Σuc (r) the event r 5 N (M, M · 2), {s1 → M, s2 → L, N (L, L · 3) The same as at the first step Q5 δ1 (M, l, L), p1 → M · 2, p2 → of this inference δ3 (M · 2, l, L · 3) L · 3, σ → l} 6 N (M, M · 2), {s1 → M, s2 → G, N (G, G · 4) The same as at the first step Q5 δ1 (M, g, G), p1 → M · 2, p2 → of this inference δ3 (M · 2, g, G · 4) G · 4, σ → g} 7 N (M, M · 2), {s1 → M, s2 → R, N (R, R · 5) The same as at the first step Q5 δ1 (M, r, R), p1 → M · 2, p2 → of this inference δ3 (M · 2, r, R · 5) R · 5, σ → r} 8 Chk(M · 2, s, 0) {p1 → M · 2, Chk(M · 2, s, 1) The check assigned in the Q3 (deleted), p2 → S · 1, step 3 is passed, i.e., viola- δ3 (M · 2, s, S · 1) σ → s} tion of controllability is not found 9 Chk(M · 2, r, 0) {p1 → M · 2, Chk(M · 2, r, 1) The check assigned in the Q3 (deleted), p2 → R · 5, step 4 is passed, i.e., viola- δ3 (M · 2, r, R · 5) σ → r} tion of controllability is not found 10 N (L, L · 3), {s1 → L, s2 → S, Chk(L · 3, s, 0) The same as in step 4, Q2 δ1 (L, s, S) p1 → L · 3, σ → s} the check assigned for the Σuc (s) event s, i.e., if there is the transition from L labeled with s there must be the same transition labeled with s in the product automaton from the state L, 2 11 N (G, G · 4), {s1 → G, s2 → R, Chk(G · 4, r, 0) Another check is assigned Q2 δ1 (G, r, R) p1 → G · 4, σ → r} for the event r which goes Σuc (r) from the state G Continued on the next page Table 1 – continued from the previous page Q Base atoms used Substitution Atoms added Step Result 12 N (R, R · 5), {s1 → R, s2 → S, Chk(R · 5, s, 0) Another check is assigned Q2 δ1 (R, s, S) p1 → R · 5, σ → s} for the event s which may Σuc (s) occur at the state R 13 Chk(L · 3, s, 0) {p1 → L · 3, Chk(L · 3, s, 1) The check assigned at the Q3 (deleted), p2 → S · 1, step 10 is passed, i.e., viola- δ3 (L · 3, s, S · 1) σ → s} tion of controllability is not found 14 Chk(G · 4, r, 0) {p1 → G · 4, Chk(G · 4, r, 1) The check assigned in the Q3 (deleted), p2 → R · 5, step 11 is passed, i.e., viola- δ3 (G · 4, r, R · 5) σ → r} tion of controllability is not found 15 Chk(R · 5, s, 0) {p1 → R · 5, Chk(R · 5, s, 1) The check assigned at the Q3 (deleted), p2 → S · 1, step 12 is passed, i.e., viola- δ3 (R · 5, s, S · 1) σ → s} tion of controllability is not found 16 N (L, L · 3), {s1 → L, s2 → C, Chk(L · 3, c, 0) The same as at the previous Q2 δ1 (L, c, C) p1 → L · 3, σ → c} step, the check assigned Σuc (c) for another uncontrollable transition from L labeled with c 17 Chk(L · 3, c, 0) {p1 → L · 3, Del(L · 3, c) The check assigned at the Q4 σ → c} previous step was failed; therefore, the specification corresponding to the au- tomaton H is uncontrol- lable. Since the tested specification is uncontrollable, the rules for deleting the transitions associated with the state found in the previous steps are triggered. 18 Del(L · 3), {p11 → L, p12 → 3, Deleted(3, s, 1) Q6 δ2 (3, s, 1), p21 → S, p22 → δ3 (L · 3, s, S · 1) 1, σ → s} 19 Del(L · 3), {p11 → L, p12 → 3, Deleted(3, g, 4) Q6 δ2 (3, g, 4), p21 → G, p22 → δ3 (L · 3, g, G · 4) 4, σ → g} Continued on the next page Table 1 – continued from the previous page Q Base atoms used Substitution Atoms added Step Result 20 Del(L · 3), {p11 → L, p12 → 3, Deleted(3, m, 2) Q6 δ2 (3, m, 2), p21 → M, p22 → δ3 (L·3, m, M ·2) 2, σ → m} 21 Del(L · 3), {p11 → M, p12 → 2, Deleted(2, l, 3) Q7 δ2 (2, l, 3), p21 → L, p22 → δ3 (M · 2, l, L · 3) 3, σ → l} 5. Supervisor realization 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 find a solution of the basic problem of supervisory control, i.e., a supervisor J and the closed- looped 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 ||G) [20]. In our formalization, the joint work of the system and the supervisor is carried out using the PCF FSC below. ∃ B, BS ∀σ, s, σ 0 , s0 L(σ, s), δ1 (s, σ 0 , s0 ), δ2 (s, σ 0 , s0 ) ∃L(σ · σ 0 , s0 ) 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 figure 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 : {L(ε, 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 )} Table 2. Generating L(J /G) for the AUV model. Q Base atoms Substitution Atoms added Step Result 1 L(ε, X1 ), {σ → ε, σ 0 → m, L(ε · m, X2 ) Adding the first event m to Q1 δ1 (X1 , m, X2 ) s → X1 , s0 → X2 } the chain of events δ2 (X1 , m, X2 ) Current chain of events: m 2 L(ε · m, X2 ), {σ → ε · m, σ 0 → s, L(ε · m · s, X1 ) Adding the next possible Q1 δ1 (X2 , s, X1 ) s → X2 , s0 → X1 } event s, which corresponds δ2 (X2 , s, X1 ) to the transition from X2 to X1 Current chain of events: ms 3 L(ε · m, X2 ), {σ → ε · m, σ 0 → g, L(ε · m · g, X4 ) Adding the next possible Q1 δ1 (X2 , g, X4 ) s → X2 , s0 → X4 } event g, which corresponds δ2 (X2 , g, X4 ) to the transition from X2 to X4 Current chain of events: mg 4 L(ε · m, X2 ), {σ → ε · m, σ 0 → r, L(ε · m · r, X5 ) Current chain of events: mr Q1 δ1 (X2 , r, X5 ) s → X2 , s0 → X5 } δ2 (X2 , r, X5 ) 5 L(ε · m · s, X1 ), {σ → ε · m · s, σ 0 → L(ε·m·s·m, X2 ) Current chain of events: Q1 δ1 (X1 , m, X2 ) m, msm δ2 (X1 , m, X2 ) s → X1 , s0 → X2 } 6 L(ε · m · g, X4 ), {σ → ε · m · g, σ 0 → L(ε·m·g·m, X2 ) Current chain of events: Q1 δ1 (X4 , m, X2 ) m, mgm δ2 (X4 , m, X2 ) s → X4 , s0 → X2 } 7 L(ε · m · g, X4 ), {σ → ε·m·g, σ 0 → r, L(ε·m·g ·r, X5 ) Current chain of events: Q1 δ1 (X4 , r, X5 ) s → X4 , s0 → X5 } mgr δ2 (X4 , r, X5 ) 8 L(ε · m · r, X5 ), {σ → ε·m·r, σ 0 → s, L(ε·m·r ·s, X1 ) Current chain of events: Q1 δ1 (X5 , s, X1 ) s → X5 , s0 → X1 } mrs δ2 (X5 , s, X1 ) 9 L(ε · m · r, X5 ), {σ → ε·m·r, σ 0 → g, L(ε·m·r·g, X4 ) Current chain of events: Q1 δ1 (X5 , g, X4 ) s → X5 , s0 → X4 } mrg δ2 (X5 , g, X4 ) 10 L(ε · m · r, X5 ), {σ → ε · m · r, σ 0 → L(ε·m·r·m, X2 ) Current chain of events: Q1 δ1 (X5 , m, X2 ) m, mrm δ2 (X5 , m, X2 ) s → X5 , s0 → X2 } 11 L(ε·m·s·m, X2 ), {σ → ε·m·s·m, σ 0 → L(ε · m · s · m · Current chain of events: Q1 δ1 (X2 , s, X1 ) s, s, X1 ) msms δ2 (X2 , s, X1 ) s → X2 , s0 → X1 } And so on... The inference will never terminate... Conclusion 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 different levels of the hierarchical control system for mobile robots. Acknowledgments 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. References [1] Wonham W M and Cai K 2019 Supervisory Control of Discrete-Event Systems (Springer International Publishing) [2] Davydov A, Larionov A and Nagul N 2017 2017 40th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO) (IEEE) pp 1161–1165 [3] Davydov A, Larionov A and Nagul N 2018 AIP Conference Proceedings 2046 020021 (Preprint https://aip.scitation.org/doi/pdf/10.1063/1.5081541) URL https://aip.scitation.org/doi/abs/10.1063/1.5081541 [4] 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 [5] Vassilyev S N 1990 The Journal of Logic Programming 9 235–266 [6] Zherlov A K, Vassilyev S N, Fedosov E A and Fedunov B E 2000 Intelligent control of dynamic systems (Moscow: Fizmatlit) in Russian [7] Davydov A, Larionov A and Cherkashin E 2011 Automatic Control and Computer Sciences 45 402–407 [8] Larionov A, Davydov A and Cherkashin E 2013 International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), Opatija 2013 1023–1028 [9] Bychkov I, Davydov A, Nagul N and Ul’yanov S 2018 Information Technology in Industry 6 20–26 [10] Bychkov I, Davydov A, Kenzin M, Maksimkin N, Nagul N and Ul’yanov S 2019 2019 International Siberian Conference on Control and Communications (SIBCON) pp 1–6 [11] Jayasiri A, Mann G and Gosine R 2011 IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics) 41 1224 – 1238 ISSN 1083-4419 [12] Torrico C R, Leal A B and Watanabe A T 2016 IFAC-Papers OnLine 49 240 – 245 ISSN 2405-8963 [13] Dai X, Jiang L and Zhao Y 2016 Applied Intelligence 45 18–29 ISSN 1573-7497 [14] Tsalatsanis A, Yalcin A and Valavanis K P 2012 Robotica 30 721––730 [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 978- 1-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)