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 brie y described. A method for constructing a product of automata using constructive inference in the positively constructed formulas calculus is proposed. Based on the given speci cation on the behaviour of the system, a method for constructing a supremal controllable sublanguage of the speci cation is presented.
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
veri cation problems ([
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 nite state automata. In the seminal
work of P. Ramage and W. Wonham [
DES, developed in authors' previous works [
The calculus of PCFs was introduced in [
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.
Consider discrete-event system (DES) in the form of a generator of a formal language [
Suppose some events of G are controllable, i.e. may be prohibited from occurring. Let c
be a controllable event set, uc = n c, c \ uc = ;. The Ramadge{Wonham supervisory
control framework assumes the existence of a means of control G presented by a supervisor [
The main goal of supervisory control is to construct such supervisor that L(J =G) = K and Lm(J =G) = K. The de nition of controllability plays a crucial role in characterizing those languages that can be generated by the closed-loop structure plant{supervisor.
De nition 1 [
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 pre x 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 speci cation is built to check if the same uncontrollable transitions present in both speci cation and the plant. The controllability checking using PCFs is illustrated in Section 5 below.
If the speci cation under consideration happen to be not controllable, a controllable part of
it may be used for designing a supervisor. Let [
Cin(K) = fL
K : L uc \ L(G)
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 [
De nition 2. [
: (9t 2 L2)[st 2 L1]g: K"C = K n [(L(G) n K)= uc]j : This formula means that if the string with the pre x 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.
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 rst-order logic that consists of rst-order formulas (FOFs) built out of atomic formulas with &; _; :; !; $ operators, 8 and 9 quanti er symbols and constants true and f alse. The concepts of term, atom, literal we de ne 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 = 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-quanti er corresponds to ! _, where _ means disjunction of all the formulas from , and 9-quanti er 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 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 .
De nition 3. Let X be a set of variables, and A be a conjunct, both can be empty. (i) 9X A is an 9-PCF, (ii) 8X A is a 8-PCF, (iii) If
= fF1; : : : ; Fng is a set of 8-PCFs, then 9X A (iv) If = fF1; : : : ; Fng is a set of 9-PCFs, then 8X A (v) Any 9-PCF or 8-PCF is a PCF, (vi) There are only PCFs of a form 9-PCF and 8-PCF. is an 9-PCF, is a 8-PCF,
The term \positively" comes from the fact that according to De nition 3 PCFs contain no negation operator :.
For the sake of readability, we represent PCFs as trees whose nodes are type quanti ers, 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 is represented as a tree as follows: 8 9X1 A1 9A5 8Y1 B1 8B2 8Y3 B4 9X2 A2 9A3 9A4 8Y2 B3
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 di erent quanti ers simultaneously.
De nition 4. [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.
De nition 5. Let P1 = 9X A and P2 = 9Y B , then merge(P1; P2) = 9X[Y A [ B [ .
De nition 6. 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) = ?.
De nition 7. [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 when the set becomes empty after applying an ! rule, and the PCF becomes just 8, then it can be concluded that the negation of an original formula is unsatis able.
Any nite sequence of PCFs F ; !F ; !2F ; : : : ; !nF , where !sF = !(!s 1F ); !1 = !; !nF = 8, is called an inference of F in PCF calculus (with the axiom 8).
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 8 9S(e) 8x S(x)
9A(x) 8x; y C(x; y) 8x A(x) 9y C(y; f (x)) 9
8x S(x); A(x) 9C(x; f (x))
At the rst step of the inference there is only one answer fx ! eg to the rst 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: 8 9S(e); A(e) Q2 Q3
At the second step there is also only one answer fx ! eg to question Q3. After applying ! with this answer, formula is split, because Q3 has disjunctive branching. The formula will have the following form, F3: where F31 is: and F32 is: 8
F 1
3 F 2
3 9y1 S(e); A(e); C(y1; f (e))
Q1 Q2
Q3 9y1 S(e); A(e)
Q1 Q2 Q3 8x S(x); A(x) 9C(x; f (x))
At the third step the rst base can be refuted by answering on Q2 (the goal question) with fx ! y1; y ! f (e)g. 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 fx ! e; y ! eg to the fourth new question of the base F32 which adds the atom C(e; f (e)) to it.
At the fth step, the only base can be refuted by answering on Q2 (the goal question) with the answer fx ! e; y ! f (e)g, nishing 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 de nition 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 a ects 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.
To formalize a nite 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 rst 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 = fI(S); L("; S); Lm("; S); (S1i; i; S2i); m(S1i; i; S2i); c( j ); uc( j )g, i 2 f1; : : : ; ng, j 2 f1; : : : ; kg, n is the number of transitions, k is the number of events, and two questions shown in gure 1. Applying the inference rules to this PCF, the words of the languages generated and marked by the automaton will be constructed as the rst 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( 0; s0) 0; s0)
Suppose that behaviour of G should be constrained within the speci cation language K, and let automaton H generates, or recognizes, K. In order to check the controllability of K, we rst 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 di erent 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 = fI1(S0); I2(P0); 1(S1i; i; S2i); 2(S1k; k; S2k)g, containing atoms for transitions 1, i = 1; n1, of the rst automaton and transitions 2, k = 1; n2, of the second one. The questions of FG H are as follows: 1 : 8s; p I1(s); I2(p) 9I3(s p) 2 : 8s; p I1(s); I2(p) 9 3( ; "; s p) 3 : 8 ; s1; p1; s2; p2; 0; s0 1(s1; ; s2); 2(p1; ; p2); 3(s0; 0; s1 p1) 9 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 rst 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 gure 4 is shown in table 1. It is assumed that the base contains atoms corresponding to transitions of the automata depicted in gure 2 and gure 3.
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 gure 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 rst 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 rst argument of this atom denotes a state p1 of H, in which the e A
C a d c b 2
e a A,1
C,3
b d c 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 speci cation, 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 speci cation, 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 speci cation 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 speci cation a controllable sublanguage is equal to the empty string alone, then during the inference all transitions in the automata corresponding to the speci cation 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 speci cation represented by the automaton shown in gure 3 with respect to the plant shown in gure 2. It is assumed that the inference of the product automaton ( gure 4) is already built, and the base from which the presented inference starts includes the next subset of atoms: fI1(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); Q4 fp1 ! D 4; Del(D 4; a) The check assigned in the ! ag previous step was failed; therefore, the speci cation corresponding to the automaton H is uncontrollable.
Since the tested speci cation is uncontrollable, the rules for deleting the transitions associated with the state found in the previous steps are triggered.
Del(D 4); 2(4; e; 2); 3(D 4; e; B 2) fp11 ! D; p12 ! 4; p21 ! B; p22 ! 2; ! eg
Above we described the approach to the representation of automata, which underlie DES in the Ramadge-Wonham SCT framework, using rst-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 speci cation 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 modi cation of speci cations, choosing controllable event set, and supervisors reduction. These and other issues will be studied in our future works.
The research is supported by the Russian Science Foundation (project no. 16-11-00053).