The construction of controllable sublanguage of specification for DES via PCFs based inference 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 considers how methods of a logical inference search in the calculus of positively constructed formulas may be applied to represent and study discrete event systems. The formalisms of discrete event systems and positively constructed formulas are briefly described. A method for constructing a product of automata using constructive inference in the positively constructed formulas calculus is proposed. Based on the given specification on the behaviour of the system, a method for constructing a supremal controllable sublanguage of the specification is presented. 1. Introduction In many applications, logical tools proved to be a mighty instrument for solving complex problems. For example, automated theorem proving (ATP) is used in various areas, including verification problems ([1, 2]), supporting research and education ([3]), and robotics ([4, 5]). In this paper, we show how ATP based on the calculus of positively constructed formulas (PCF) helps to solve one of the problems arising in supervisory control theory (SCT) for discrete event systems (DES). The term discrete event system appeared in the early 1980s and denoted a wide class of systems with discrete states whose evolution is driven by the occurrence of some discrete events. The most common and convenient way to represent DES is finite state automata. In the seminal work of P. Ramage and W. Wonham [6] the theory for DES control was established. Some events of automata-based DES are supposed to be prohibited from occurring to restrict system behaviour within constraints given by some specification. The means of such control is called a supervisor. The problem of designing a proper supervisor for fully or partially observed DES is the main problem of SCT. Controllability of specification is a crucial property which must be verified to start building a supervisor. It may be compared to the safety property of the controlled system: no uncontrolled event which is not allowed by specification may occur. In the case when the specification is not controllable, controllable sublanguage of this specification may be found as a new admissible specification. Although there is a well-known algorithm of building controllable sublanguage (see, e.g. [7]), we suggest a new approach to this problem, based on the ATP in the PCF calculus. This approach is a part of a new method of dealing with Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). DES, developed in authors’ previous works [8, 9, 10]. It allows one to solve SCT problems more effectively via the use of additional information accumulated in the process of the inference. The calculus of PCFs was introduced in [11] and further developed in [12] and [13] as a complete method for ATP with functional symbols. The most important features of the PCF calculus and its implementation in the prover are the following: 1) large block data structures for representing formulas and inference rules; 2) no need of removing existence quantifiers by the skolemization procedure, which increases the complexity of the formula; 3) compatibility with specific application heuristics, as well as with general inference control heuristics; 4) logical inference is easy to read, which helps to find errors in formalization more quickly; 5) support for equality; 6) modifiability of semantics, support for non-classical logics. A detailed discussion of characteristics and features of the calculus may be found in [13]. The rest of the paper is organized as follows. The introductory notes on DES and SCT are provided in the next section. The third section contains a brief description of PCFs and the PCF calculus. In Section 4, a way of automata-based DES representation as PCF is described. In Section 5, a method for a supremal controllable sublanguage of a given language construction is presented. Some remarks on the results obtained are made in Conclusion. 2. Supervisory control of DES Consider discrete-event system (DES) in the form of a generator of a formal language [6] G = (Q, Σ, δ, q0 , Qm ), also called a plant in the automatic control theory. 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. Let Σ∗ denote the set of all strings over Σ, including the 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. Suppose some events of G are controllable, i.e. may be prohibited from occurring. Let Σc be a controllable event set, Σuc = Σ \ Σc , Σc ∩ Σuc = ∅. The Ramadge–Wonham supervisory control framework assumes the existence of a means of control G presented by a supervisor [6]. 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. Denote L(J /G) a language generated by the closed-looped behavior of the plant and the supervisor. 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 plays a crucial role in characterizing those languages that can be generated by the closed-loop structure plant–supervisor. Definition 1 [6] K is controllable (with respect to L(G) and Σuc ) if KΣuc ∩ L(G) ⊆ K. If K represents the admissible behaviour of the system, K is controllable if occurring of any uncontrolled event after a prefix of a word from K leads to a word from K, i.e., still admissible. Only controllable languages may be exactly achieved by the joint behaviour of the plant and supervisor. 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 specification and the plant. The controllability checking using PCFs is illustrated in Section 5 below. If the specification under consideration happen to be not controllable, a controllable part of it may be used for designing a supervisor. Let [7] Cin (K) = {L ⊆ K : LΣuc ∩ L(G) ⊆ L} be a set of all controllable sublanguages of a given language K. 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. Following [7], denote this language K ↑C . To obtain K ↑C for a prefix-closed K, a quotient structure of automata is used. Definition 2. [7] The quotient operation for languages L1 , L2 ⊆ Σ∗ is defined as L1 /L2 := {s ∈ Σ∗ : (∃t ∈ L2 )[st ∈ L1 ]}. The exact formula for computing K ↑C for a prefix-closed K is then as follows: K ↑C = K \ [(L(G) \ K)/Σ∗uc ]|Σ∗ . This formula means that if the string with the prefix belonging to K has an uncontrollable continuation leading it out of K, it should be excluded from K. In the next sections, we construct K ↑C with the help of logical inference in the PCF calculus using the PCF representation of automata. 3. The calculus of positively constructed formulas In the process of reasoning in the natural language, one often proves some statement by refuting the contradictory statement. We intend to proceed similarly. The main idea of the PCF calculus is to refute the negation of a formula F to prove that F is valid. 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.), possibly 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 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 formula formalization. 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 3. 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. Definition 4. [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 5. Let P1 = ∃X A Ψ and P2 = ∃Y B Φ, then merge(P1 , P2 ) = ∃X∪Y A ∪ B Ψ ∪ Φ. Definition 6. 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 7. [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 when the set Φ becomes empty after applying an ω rule, and the PCF becomes just ∀, then it can be concluded that the negation of an original formula is unsatisfiable. 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 PCF calculus (with the axiom ∀). Suppose that a search strategy does not use repeated application of ω to a question with the same θ (question-answering method of automated inference). Example 1. [A refutation in PCFs]. Consider the PCF F1 ∀x S(x) ∃A(x) ∀x, y C(x, y) ∀ ∃S(e) ∃y C(y, f (x)) ∀x A(x) ∃ ∀x S(x), A(x) ∃C(x, f (x)) At the first step of the inference there is only one answer {x → e} to the first question (top to bottom numbering, name it Q1 ). After applying rule ω with this answer to the only base of F1 , the formula will be converted to the following form, F2 : Q1 ∀ ∃S(e), A(e) Q2 Q3 At the second step there is also only one answer {x → e} to question Q3 . After applying ω with this answer, formula is split, because Q3 has disjunctive branching. The formula will have the following form, F3 : F31 ∀ F32 where F31 is: Q1 ∃y1 S(e), A(e), C(y1, f (e)) Q2 Q3 and F32 is: Q1 Q2 ∃y1 S(e), A(e) Q3 ∀x S(x), A(x) ∃C(x, f (x)) At the third step the first base can be refuted by answering on Q2 (the goal question) with {x → y1 ; y → f (e)}. The refuted base (and its whole base subformula) is to be deleted from the list of the base subformulas. At the fourth step there is the answer {x → e, y → e} to the fourth new question of the base F32 which adds the atom C(e, f (e)) to it. At the fifth step, the only base can be refuted by answering on Q2 (the goal question) with the answer {x → e; y → f (e)}, finishing refutation because all the bases were refuted. One of the essential features of the calculus of PCFs which will be used later is that we can build a nonmonotonic 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 always ends. 4. PCF representation of automata To formalize a finite state machine as a generator of a formal language, the following predicates will be used. Let L(s, S) denote “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. 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 1. Applying the inference rules to this PCF, the words of the languages generated and marked by the automaton will be constructed as the first arguments of the atoms L(s, S), Lm (s, S) in the base. ∀σ, 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 1. General form of PCF representation of some automaton. Suppose that behaviour of G should be constrained within the specification language K, and let automaton H generates, or recognizes, K. In order to check the controllability of K, we first build a product of automata G and H, on the basis of which further inference will be arranged. The PCF representation of constructing the product of two automata may also be written using a single formula where indices distinguish atoms corresponding to different automata. The inferences will be based on the reasoning about the structures of automata which are involved in the product. The PCF FG×H constructing the product of automata will consist 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 first automaton and transitions δ2 , k = 1, n2 , of the second one. The questions of FG×H are as follows: 1 : ∀s, p I1 (s), I2 (p) − ∃I3 (s · p) 2 : ∀s, p I1 (s), I2 (p) − ∃δ3 (ξ · ρ, ε, s · p) 3 : ∀σ, s1 , p1 , s2 , p2 , σ 0 , s0 δ1 (s1 , σ, s2 ), δ2 (p1 , σ, p2 ), δ3 (s0 , σ 0 , s1 · p1 ) − ∃δ3 (s1 · p1 , σ, s2 · p2 ) Index 1 in the subscripts of atoms of this formula corresponds to the atoms of the automaton G, 2 to the H, and 3 to the atoms corresponding to 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 2. [Product construction] The steps of the inference that constructs the automaton depicted in figure 4 is shown in table 1. It is assumed that the base contains atoms corresponding to transitions of the automata depicted in figure 2 and figure 3. Table 1. Constructive inference for the product of two automata. Q Base atoms Substitution Atoms added Result 1 I1 (A), I2 (1) {s → A, p → 1} I3 (A · 1) A,1 Continued on the next page Table 1 – continued from the previous page Q Base atoms Substitution Atoms added Result 2 I1 (A), I2 (1) {s → A, p → 1} δ 3 (ξ · ρ, ε, A · 1) A,1 3 δ 3 (xi · ρ, ε, A · 1), {s1 → A, p1 → 1, δ 3 (A · 1, a, C · 3) δ 1 (A, a, C), σ → a, s2 → C, δ 2 (1, a, 3) p2 → 3} 3 δ 3 (A · 1, a, C · 3), {s1 → C, p1 → 3, δ 3 (C · 3, b, B · 2) δ 1 (C, b, B), σ → b, s2 → B, δ 2 (3, b, 2) p2 → 2} 3 δ 3 (C · 3, b, B · 2), {s1 → B, p1 → 2, δ 3 (B · 2, c, A · 1) δ 1 (B, c, A), σ → c, s2 → A, δ 2 (2, c, 1) p2 → 2} 3 δ 3 (A · 1, a, C · 3), {s1 → C, p1 → 3, δ 3 (C · 3, d, D · 4) δ 1 (C, d, D), σ → d, s2 → D, δ 2 (3, d, 4) p2 → 4} 3 δ 3 (C · 3, d, D · 4), {s1 → D, p1 → 4, δ 3 (D · 4, e, B · 2) δ 1 (D, e, B), σ → e, s2 → B, δ 2 (4, e, 2) p2 → 2} 5. Supremal controllable sublanguage construction using a PCF inference In this section, with the help of logical inference in the PCF calculus, on the base of G × H, we construct K ↑C during the checking controllability of K. Note that in the worst case K ↑C = ∅ while in the best way K ↑C = K. Suppose that the base of PCF F contains predicate descriptions of transitions of G, H and G × H. Let the questions to the base of F be as depicted in figure 5. In these rules, states which are simultaneously achieved from the states of G and G × H by the same event are called the neighbouring states and stored as the arguments of the predicate N ( , ). The rules are to be interpreted as follows. 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. Although such s1 , p1 are not neighboring states in our sense, N (s1 , p1 ) with them is necessary for further inference. Q2 checks if there is an uncontrollable transition from some state of the automaton corresponding to the plant. Upon successful answer to this question, the atom Chk(p1 , σ, 0) is added to the base. The first argument of this atom denotes a state p1 of H, in which the 4 D d a d e 3 e C E e b a b a b 1 c 2 A c B Figure 2. Generator G. Figure 3. Recognizer H for the specification K. D,4 d C,3 e a b A,1 B,2 c Figure 4. The product of G and H. 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) − ∃ Del(p1 ) Q5 : ∀s1 , s2 , p1 , p2 , σ N (s1 , p1 ), δ1 (s1 , σ, s2 ), δ3 (p1 , σ, p2 ) − ∃ N (s2 , p2 ) Q6 : ∀p11 , p12 , p21 , p22 , σ Del(p11 · p12 ), δ2∗ (p12 , σ, p22 ), δ3∗ (p11 · p12 , σ, p21 · p22 )− − ∃ Deleted(p12 , σ, p22 ) ∗ ∗ Q7 : ∀p11 , p12 , p21 , p22 , σ Del(p21 · p22 ), δ2 (p12 , σ, p22 ), δ3 (p11 · p12 , σ, p21 · p22 )− − ∃ Deleted(p12 , σ, p22 ) Figure 5. Questions of the PCF F. transition labelled by the uncontrollable event σ should exist for K to be controllable. By default we suppose that the transition does not exist, so the third argument in Chk() is 0 before checking by the next rule. Q3 is aimed to check 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. With the help of ∗ operator, we delete the atom Chk(p1 , σ, 0) from the base. Q4 checks if the atom Chk(p1 , σ, 0) is present in the base. The presence of Chk(p1 , σ, 0) in the base means that an uncontrollable event is not allowed by the specification, i.e., K is not controllable. So the atom Del(p1 ) is added to the base upon a successful answer. It contains information about the state (p1 ) which has the event (σ) that violate the controllability condition. This atom is further used in questions Q6 , Q7 to delete transitions associated with the state p1 . Q5 adds the next checked pair of states to continue the inference search. A pair of states s2 , p2 , which are simultaneously achieved from the previously checked states of G and G × H by the same event, is added to the base as the arguments of the predicate N (s2 , p2 ). The rules Q6 , Q7 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, Q6 removes all transitions leaving this state and Q7 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 Q1 to Q7 . The rules Q1 - Q5 check whether the specification is controllable or not. The rules Q6 , Q7 remove transitions associated with the state in which an event occurs that violates the controllability condition. If during the application of the Q1 - Q5 rules the answer to question Q4 was found, an atom Del() denoting uncontrollability of K is added to the base. Then we apply the rules Q6 , Q7 , ignoring the rules from the Q1 - Q5 , until possible substitutions for applying the inference rule to Q6 and Q7 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 equal to the empty string alone, then during the inference all transitions in the automata corresponding to the specification will be deleted. Consider this strategy with the example. Example 3. Table 2 shows the inference of the PCF, which constructs the sublanguage of the specification represented by the automaton shown in figure 3 with respect to the plant shown in figure 2. It is assumed that the inference of the product automaton (figure 4) is already built, and the base from which the presented inference starts includes the next subset of atoms: {I1 (A), I3 (A · X), Σuc (a), δ1 (A, a, C), δ1 (C, e, A), δ1 (B, c, A), δ1 (C, b, B), δ1 (C, d, D), δ1 (D, e, B), δ1 (D, a, E), δ1 (E, b, B), δ2 (1, a, 3), δ2 (2, c, 1), δ2 (3, b, 2), δ2 (3, d, 4), δ2 (4, e, 2), δ3 (A · 1, a, C · 3), δ3 (B · 2, c, A · 1), δ3 (C · 3, b, B · 2), δ3 (C · 3, d, D · 4), δ3 (D · 4, e, B · 2)} Table 2. Constructive inference building the controllable sublanguage of the specification. Q Base atoms used Substitution Atoms added Step Result Q1 I1 (A), I3 (A · 1), {s1 → A, s2 → C, N (A, A · 1) The pair of states A and δ1 (A, a, C), p1 → A · 1, p2 → (A, 1) in the automata G δ3 (A · 1, a, C · 3) C · 3, and G × H is to be checked σ → a} for violation controllability Continued on the next page Table 2 – continued from the previous page Q Base atoms used Substitution Atoms added Step Result Q2 N (A, A · 1), {s1 → A, s2 → C, Chk(A · 1, a, 0) In automaton G an uncon- δ1 (A, a, C) p1 → A · 1, σ → a} trolled transition label by Σuc (a) the event a was found, i.e. the check of the correspond- ing transition in the au- tomaton G × H is necessary Q3 Chk(A · 1, a, 0) {p1 → A · 1, Chk(A · 1, a, 1) The check assigned in the (deleted), p2 → C · 3, previous step is passed, i.e. δ3 (A · 1, a, C · 3) σ → a} violation of controllability is not found Q5 N (A, A · 1), {s1 → A, s2 → C, N (C, C · 3) The same as at the first step δ1 (A, a, C), p1 → A · 1, p2 → of this inference δ3 (A · 1, a, C · 3) C · 3, σ → a} Q5 N (C, C · 3), {s1 → C, s2 → B, N (B, B · 2) ... δ1 (C, b, B), p1 → C · 3, p2 → δ3 (C · 3, b, B · 2) B · 2, σ → b} Q5 N (C, C · 3), {s1 → C, s2 → D, N (D, D · 4) ... δ1 (C, d, D), p1 → C · 3, p2 → δ3 (C · 3, d, D · 4) D · 4, σ → d} Q2 N (D, D · 1), {s1 → D, s2 → E, Chk(D · 4, a, 0) The same as at the second δ1 (D, a, E) p1 → D · 4, σ → a} step of this inference Σuc (a) Q4 Chk(D · 4, a, 0) {p1 → D · 4, Del(D · 4, a) The check assigned in the σ → a} 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. Q6 Del(D · 4), {p11 → D, p12 → 4, Deleted(4, e, 2) δ2 (4, e, 2), p21 → B, p22 → δ3 (D · 4, e, B · 2) 2, σ → e} Q7 Del(D · 4), {p11 → C, p12 → 3, Deleted(3, d, 4) δ2 (3, d, 4), p21 → D, p22 → δ3 (C · 3, d, D · 4) 4, σ → d} Conclusion Above we described the approach to the representation of automata, which underlie DES in the Ramadge-Wonham SCT framework, using first-order logical formulas of the PCF language. The method for building a product of automata in the process of the constructive inference of the PCF is proposed. Based on the specification on the behavior of DES, given in the form of a regular language, a method for constructing its supremal controllable sublanguage is presented. The knowledge, accumulated in the base of the PCF during the inference, may be employed for solving various problems of SCT, including modification of specifications, choosing controllable event set, and supervisors reduction. These and other issues will be studied in our future works. Acknowledgments The research is supported by the Russian Science Foundation (project no. 16-11-00053). References [1] Lockhart J, Purdy C and Wilsey P A 2017 2017 IEEE National Aerospace and Electronics Conference (NAECON) pp 358–361 [2] Shiraz S and Hasan O 2018 Formal Methods: Foundations and Applications ed Massoni T and Mousavi M R (Cham: Springer International Publishing) pp 74–89 ISBN 978-3-030-03044-5 [3] Frank M and Kreitz C 2018 Electronic Proceedings in Theoretical Computer Science 267 59–69 [4] Erdem E and Patoglu V 2018 KI - Künstliche Intelligenz 32 [5] Nalepa G J 2018 Designing Robot Control Logic with Rules (Cham: Springer International Publishing) pp 381–401 ISBN 978-3-319-66655-6 [6] Ramadge P J and Wonham W M 1987 SIAM Journal on Control and Optimization 25 206–230 [7] Cassandras C G and Lafortune S 2008 Introduction to Discrete Event Systems (Springer US) [8] 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 [9] 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 [10] 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 [11] Vassilyev S N 1990 The Journal of Logic Programming 9 235–266 [12] Davydov A, Larionov A and Cherkashin E 2011 Automatic Control and Computer Sciences 45 402–407 [13] Larionov A, Davydov A and Cherkashin E 2013 International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), Opatija 2013 1023–1028