The paper demonstrates how the automatic theorem proving technique of the PCF calculus is applied to construct parallel composition of automata. Parallel composition plays an essential role in the supervisory control theory at di erent stages of systems and supervisors design. Improved formalization of discrete event systems as positively-constructed formulas along with auxiliary predicates, serving for accessibility of the automaton checking, simplify parallel composition construction.
This paper continuous the series of works developing a new way to deal with discrete-event
systems (DES). Being subject to Ramage-Wonham supervisory control theory (SCT) for DES,
a physical system and requiments to system`s behavior are usually modeled by one or several
nite state automata, sometimes called free behavior models and speci cations. Nodes of
the state transition diagrams of the automata involved correspond to essential states of the
system while edges correspond to events leading to changes of the states. Then, in the SCT
framework, a supervisor as a means of control is built to guarantee the speci cations ful llment.
In previous papers the application of automated theorem proving based on the
positivelyconstructed formulas (PCF) to the formalization of DES [
The PCF calculus is developed in [
Since more and more complicated systems are modeled as DES to apply SCT results and
obtain control required, such DES are usually constructed as sets of automata where each
automaton corresponds to some aspect of physical system`s functioning. For example, in [
In [
The examples above show that parallel composition as one of composition operations on
automata plays a very important role in SCT. After a supervisor has been designed, behavior
of the system under its control is described by the parallel composition of the automaton
representing uncontrolled behavior and the automaton of the supervisor. Parallel composition
also serves for checking controllability of a speci cation language and helps to design supervisor
if speci cation occurs to be controllable. Target language [
The current paper demonstrates how the PCF calculus is applied to construct parallel composition using logical inference only. The rest of the paper is organized as follows. In the next section the basic notion of the automata-based DES with a small example of the parallel composition of automata is provided. The third section contains brief description of PCFs and the PCF calculus. In section 4 main features of the PCF calculus are discussed. The PCFformalization of parallel composition is given in section 5. Application of the results obtained are discussed in Conclusions.
The rst [
As well known, two operations are used to compose automata: product and parallel, or synchronous, compositions. In SCT parallel composition is used in supervisor constructing algorithms, for checking controllability, to construct system behavior under control of the supervisor. Moreover, since complex systems are usually designed using modular architecture, with each module having its special functionality, generator G may correspond to one of these modules. Parallel composition then serves to compose system model from models of separate modules. Leaving SCT applications for future work, in what follows general notion of parallel composition of deterministic automata, as used to built complex system, is considered.
De nition 1 [Parallel composition] If two generators Gi = (Qi; i; i; q0i; Qim), i = 1; 2, are
given then parallel composition is de ned [
In the parallel composition of two automata events shared by the automata must occur concurrently. Thus the automata are synchronized by the common events. Events that are not shared by the automata may occur independently. Using the same principle, above de nition 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 de ned using associativity: G1jjG2jjG3 := (G1jjG2)jjG3.
Example 1. Consider two state transition diagrams in gures 1 and 2. Initial states are marked with arrows while double circles denote marked states. The automaton in gure 3 is the result of the parallel composition of the automata in gures 1 and 2.
a A a b
C c b b
B
B,Y
Before operation Ac implementation, the resulting automaton has 6 states. Three of them are inaccessible. Attention should be paid to the missing self-loop over b at the state (B; Y ). The fourth rule of (1) is applied in this case since the event b is shared by automata but 2(b; Y ) is unde ned. In section 5 this example will be formalized by PCFs. Note that G2 may be considered as a speci cation for G1.
Consider a language of a 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 a term, an atom, and a literal are de ned in the usual way. Nonatomic formulas and subformulas will be denoted further by capital calligraphic letters (F ; P; Q, etc.), possibly with indices. Sets of formulas will be denoted by capital Greek 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 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, respectively. 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 an empty disjunction is identical to f alse whereas an empty conjunction is identical to true, the following equivalences are correct: 8X A ? 8X A ! f alse 8X A, 9X A ? 9X A&true 9X A, 8? true ! 8 , and 9? true& 9 .
The constructions 8X A and 9X A are called positive type quanti ers (TQ) because A is a conjunction of positive atoms only and referred to as type condition for X. In practice, these constructions denote phrases such as \for all X satisfying A there is...", \there exists X satisfying property A such that...", and so on; for example, \for all integer x; y; z and n > 2 there is xn + y 6
n = zn". Originally, the term \type quanti er" was introduced by N. Bourbaki [
Then (i) 9X A and 8X A are 9{PCF and 8{PCF, respectively. (ii) If F = fF1; : : : ; Fng is a set of 8{PCFs then 9X A : F is 9{PCF. (iii) If F = fF1; : : : ; Fng is a set of 9{PCFs then 8X A : F is 8{PCF. (iv) Any 9{PCF or 8{PCF is PCF.
This form of logical formulas is referred to as positively constructed formulas (PCFs) as they
are written with positive type quanti ers only and do not contain the explicit logic negation
sign. Without loss of generality only closed formulas will be considered. Any FOF may be
represented as PCF [
PCF starting with 8? is called PCF in the canonical form. Any PCF can be represented in the canonical form. If F is a non{canonical 9{PCF then 8? : F is the canonical PCF since 8? : F true ! F F . If F is a non{canonical 8{PCF then the canonical PCF is 8? : f9? : F g true ! true&F F . Type quanti ers 8? and 9? are called ctitious since they do not in uence truth value of the original PCF and do not bind any variables. They are used to regularize PCFs, i.e. transform them to the canonical ones.
For the sake of readability we represent PCFs as trees whose nodes are type quanti ers, and we use corresponding names: node, root, leaf, branch. For example, PCF
8 f9X1 A1 f8Y1 B1; 8B2 f9X2 A2; 9A3 f8Y2 B3g; 9A4gg; 9A5 f8Y3 B4gg may be represented as a tree 8 9X1 A1 9A5 8Y1 B1 8B2 8Y3 B4: 9X2 A2 9A3 9A4 8Y2 B3
Parts of a canonical PCF are named as follows: (i) The root of a canonical PCF's tree-view 8? is called a PCF root. (ii) Each PCF root child 9X A is called a PCF base, the conjunct A is called base of facts, and
PCF rooted from the base is called a base subformula. (iii) PCF base children 8Y B are called questions to the parent base. If a question is a leaf of a tree then it is called a goal question. (iv) Subtrees of questions are called consequents.
In the process of reasoning one often proves a statement F by refuting its negation. We intend to proceed similarly.
De nition 3 [Answer] A question 8Y D : to a base 9X A has an answer if and only if is a substitution Y ! H1 [ X and D A, where H1 is Herbrand universe based on constant and function symbols that occur in corresponding base subformula.
De nition 4 [Splitting] Let B = 9X A : , and Q = 8Y D : , where = f9Z1 C1 : 1; : : : ; 9Zn Cn : ng then split(B; Q) = f9X[Z10 A[C10 : [ 10; : : : ; 9X[Zn0 A[Cn0 : [ n0g, where 0 is a variable renaming operator. We say that B is split by Q. Obviously, split(B; 8Y D) = split(B; 8Y D : ?) = ?.
De nition 5 [Inference rule !] Consider some canonical PCF F = 8? : . Let there exist a question Q that has an answer to appropriate base B 2 . Then !F = 8? : n fBg [ split(B; Q ).
In other words, if a question has an answer to its base then the base subformula is split by this question. In the case of a goal question we say that the basic subformula is refuted because split(B; 8Y D) = ?. The refuted base subformula B is removed from the set of base subformulas since n fSg [ ? = n fSg. Note that when the set becomes empty after applying ! rule and PCF becomes just 8 then it can be concluded that the negation of the original formula is unsatis able.
Any nite sequence of PCFs F , !F , !2F , : : :, !nF , where !sF = !(!s 1F ), !1 = !; !nF = 8, is called a deduction of F in the PCF calculus (with the axiom 8). Suppose that a search strategy veri es the questions in consecutive order, without omissions (i.e. the veri cation is repeated only when the whole list of questions was used), and it does not use several applications of ! to a question with the same (question-answering method of automated deduction).
At the rst step of the inference there is the only answer fx ! eg to the rst question (name it Q1, from the top to the bottom numbering is used). After applying the rule ! with this answer to the only base of F1, the formula is converted to the form F2:
F1 = 8
9S(e) F2 = 8 9S(e); A(e) 8x S(x) 8x; y C(x; y) 8x A(x) 8x S(x) 8x; y C(x; y) 8x A(x) 9A(x) 9y C(y; f (x)) 9 8x S(x); A(x)
9C(x; f (x)) 9A(x) 9y C(y; f (x)) 9 8x S(x); A(x) 9C(x; f (x))
At the second step there is also only one answer fx ! eg to the question Q3. After applying ! with this answer, F2 is split because Q3 has the disjunctive branching. The formula gets the form F3:
F3 = 8 9y1 S(e); A(e); C(y1; f (e)) 9y1 S(e); A(e)
Q1 Q2 Q3 Q1 Q2 Q3 8x S(x); A(x) 9C(x; f (x))
At the third step the rst base can be refuted by answering to 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 second base which adds the atom C(e; f (e)) to it.
At the fth step the only base can be refuted by answering to Q2 (the goal question) with the answer fx ! e; y ! f (e)g. This nishes refutation because all the bases were refuted.
Consider main features of the PCF language. First of all, unlike predicate calculus language
syntax, PCFs have rather unconventional and exquisite form:
(i) Any formula written in the PCF language is characterized by a large-block structure and
contains only positive quanti ers.
(ii) Any PCF has a simple and regular structure, i.e. the formula to some extent is characterized
by predictability of its structure determined by the order of 9- and 8-nodes which alternate
at each branch.
(iii) The negation of PCF is merely obtained by the replacement of the symbol 9 with 8, and
vice versa (after what canonization follows).
(iv) The PCF-representation is more compact than the representation in terms of the well known
language of clauses [
Consider features (iv){(vi) in greater detail with the help of the following example. Example 3. The FOF
8x(A& ! (9y1 B1& _ : : : _ 9yk Bk&)); where Bi& = C1i & : : : &Cni; A& = A1& : : : &Al; i = 1; k; in terms of the PCF-representation has l + n k atoms. In terms of the language of clauses it takes the form (i1;:::;ik)2(1;n)k(:A1 _ : : : _ :Al _ Ci11 _ : : : _ Cikk );
& i.e. contains (l + k)nk atoms (nk clauses). It is also obvious that, except of the auxiliary quanti ers, the number of atoms in the PCF-representation is not larger than in any classical disjunctive (conjunctive) normal form. Moreover, the representation (3) of the initial formula (2) is not only more complicated but also substantially destroys the structure of (2), although in the language of PCFs the initial structure of (2) is saved: (2) (3)
The language of clauses has been used in the resolution method [
Below we list quite important advantages of PCF calculus which are due not only to the features of the PCF language, but also to the proper deductive power of the calculus. (i) Unlike that in many other known logic calculi, e.g. those of Hentzen type, the PCF calculus has only one inference rule !. Availability of the only rule narrows the combinatorial space. However, this is not the main advantage of the calculus. The set of important merits of the PCF calculus includes not only uniqueness of its inference rule but also its unary character (e.g., in comparison with the resolution method). Another advantage of the PCF calculus, obvious from the view-point of decrescence of combinatorics, is that the inference rule ! is a large-block one, likewise the language of the PCF calculus itself. Such a rule leads to additional reduction of complexity of the combinatorial space (unlike that of the resolution rule which is also unique but is binary and a small-block one). (ii) The deduction (refutation) technique described has centered on application of ! to the questions only, i.e. to the successors of PCF roots. Application of ! to questions only is based on the properties (i), (ii) of the PCF language and allows one to focus the attention of the technique on the local fragments of PCF, without any loss of completeness of the technique. (iii) The deduction technique can be described in pithy terms of the question-answering procedure instead of technical terms of formal deducibility (i.e. in terms of logic connectives, atoms, etc.). (iv) Owing to properties (i), (ii), (vi) of the PCF language and (ii), (iii) of the PCF calculus, the deduction technique is quite compatible with heuristics of speci c applications as well as with general heuristics of control of deduction. Owing to (i), the deduction process consists of large-block steps, so is well observable and controllable. (v) The deduction technique o ers natural OR-parallelism, because the refutations of basic subformulas are executed independently of one another. (vi) The deductions obtained are quite interpretable by man owing to properties (iii), (iv). This interpretability is quite important from the viewpoint of man-machine applications. So, conceptually, the language and the calculus of PCFs are not only machine-oriented, but also human-oriented: the implementation of these techniques for the purpose of speci c applications may use these two capabilities to some greater or lesser extent. (vii) Due to the features of the PCF language and calculus, the PCF formalism has another very important merit: its semantics can be modi ed without any changes of the axiom 8 and the inference rule !. Such modi cations are implemented merely by some restrictions of applying ! and allow one to transform classical semantics of the PCF calculus in nonmonotonous semantics, constructive (intuitionistic) semantics, etc.
All these features are useful for formalizing the discrete event systems since the special structure and convenient way of inference search make it possible to describe the automata underlying the DES and to customize the inference strategies.
In order to formalize a generator representing DES, the following predicates will be used. Let L(s; S) denote \s is a current sequence of events in a state S" and Lm(s; S) denote \s is a current sequence of events in a state S, and s is a string of a marked language". Thus, rst arguments of these atoms accumulate the strings of corresponding languages, generated and marked by the automaton. Atoms of the form (S1; e; S2) will be interpreted as automaton transitions from a state S1 to a state S2 with an event e. If the right state of a transition is marked, then delta atoms with an index is used, i.e. m(S1; e; S2) if S2 is a marked state. The function symbol \ " denotes strings concatenation, and the \"" symbol corresponds to the empty string.
Behavior of a generator, representing some DES, may be simulated using the logical inference of a PCF which has the general structure depicted in gure 4.
9 L("; S0); (S1; e; S2); Lm("; S0); m(S1; e; S2) 8 ; s; e; s0 L( ; S); (s; e; s0)
9L( 8 ; s; e; s0 L( ; S); m(s; e; s0) 9Lm(
This way of formalization of a generator is more compact than the one previously suggested [
Example 4. Consider the automaton G1 from example 1 in section 2. The base of the PCF corresponding to transitions of G1 looks as
L("; A); (A; a; A); (A; b; B); (A; c; C); (B; a; A); (B; b; B); (C; b; B); Lm("; A); m(A; a; A); m(A; b; B); m(B; a; A); m(B; b; B); m(C; b; B): (G1P CF ) Recall that the base of the PCF is a set of atoms, but we arrange them, aligned and grouped in meaning, for clarity. Questions that generate the strings of the languages L(G1), Lm(G1) are the same as in the PCF on gure 4.
An inference constructing is demonstrated on the example of PCF for the automaton G2, which has the following base:
L("; X); (X; b; Y ); (X; a; X); (Y; a; X); m(X; b; Y ): (G2P CF ) Table 1 describes the inference of PCF with the base G2P CF . The rst column contains the number of a question, an answer to which is used. The second column contains a -atom used for the answer search. In the third column a corresponding substitution (answer) is presented. The fourth column contains atoms derived and added to the base, in this case, L(: : : ; : : :) and Lm(: : : ; : : :). The rst arguments of these atoms are the strings of the languages L(G2) and Lm(G2). The strategy used to build the inference is to answer both questions with the current contents of the base, if possible.
Table 1 { continued from the previous page Base atoms Substitution Atoms added m(X; b; Y ) f ! "; s ! X; e ! b; s0 ! Y g Lm(b; Y ) (X; a; X) f ! "; s ! X; e ! a; s0 ! Xg L(a; X) (Y; a; X) f ! b; s ! Y; e ! a; s0 ! Xg L(ba; X) m(X; b; y) f ! a; s ! X; e ! b; s0 ! Y g Lm(ab; Y ) (X; b; y) f ! ba; s ! X; e ! b; s0 ! Y g L(bab; Y ) m(X; b; y) f ! ba; s ! X; e ! b; s0 ! Y g Lm(bab; Y ) (X; a; X) f ! ba; s ! X; e ! b; s0 ! Xg L(baa; X)
and so on...
The goal is to build parallel composition of automata without going beyond the framework of a formal logic, i.e. it is necessary to construct a composition of automata using a logic inference, having their PCF-formalized representations. Consider two PCFs, F1 and F2, similar to the one in gure 4, representing some generators G1 and G2. To separate di erent automata in the combined base, atoms are indexed with the numbers of PCFs. To obtain PCF representing G1jjG2, we combine bases and questions of F1 and F2, and add new questions that represent the rules of (1) in de nition 1 (section 2). PCF in gure 5 is a combined formula whose inference builds the languages of automata G1, G2, and also adds new atoms in the base that correspond to transitions of G1jjG2 including marked transitions.
Let us describe the strategy that allows one to stop the inference in the most reasonable way. If the questions are numbered from the top to the bottom, then the rst four of them are the questions generating strings of the languages L(Gi), Lm(Gi), i = 1; 2, and the strategy for answering these questions remains the same. Question 5 is used only once: it adds to the base the initial state of the composition automaton. Question 6 adds a starting atom for further construction of transitions and is also used once. A pair of questions 7 and 8 corresponds to the rst rule of (1), which handles transitions over events common to both automata. Questions 9 and 10 correspond to the second rule of (1), and are aimed to handle events that belong to the alphabet of the automaton G1 only. Questions 11 and 12 handle events which belong exactly to the alphabet of the second automaton. To determine sets 1 \ 2, 1 n 2, and 2 n 1 computable predicates are used. Their computation in this case is an elementary action since the alphabets of both automata are known, however, if desired, these actions can be carried out within the logical inference.
Obviously, the answers to questions 7-12 form a nite set and are exhausted as the composition automaton is constructed. According to the strategy of inference search, after answering questions 5 and 6 the inference uses questions 7-12 only until all of their answers have been exhausted, then they may be omitted from using. It should be noted that the formula on gure 5 can be used to obtain languages for the constructed composition, if we add a pair of questions similar to the rst four, which generate languages of the automata G1 and G2.
Example 5. An example of constructing parallel composition of automata with the help of a constructive inference in the PCF calculus is given for the automata G1 and G2 from example 1 (section 2). Bases G1P CF and G2P CF are indexed as mentioned above and the inference is constructed using the questions depicted in gure 5. The inference with the corresponding composition automaton drawing is depicted in table 2. 8 ; s; e; s0 L1( ; S); m1(s; e; s0) 8 ; s; e; s0 L2( ; S); 2(s; e; s0) 8 ; s; e; s0 L2( ; S); m2(s; e; s0) 8s; p L1("; s); L2("; p) 8s; p L1("; s); L2("; p) ! ! m1(A; b; B), m2(X; b; Y ) 3("; "; AX), 1(A; c; C) fs1 ! X; ! B; p2 ! Y g
A; p1 b; s2 ! ! fs1 ! A; p1 ! X;
! c; s2 ! Cg
Thus, a method has been developed for constructing the parallel composition of automata using only constructive logical inference of PCF. The advantage of this method 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 in questions 7{12 where index i is a parameter that takes any of the values f1; 2; 3g and the symbols \ " correspond to variables, i.e. placements for the substitution of any terms.
The parallel composition of automata, wildly employed in SCT, was considered in this paper as a part of the automatic theorem proving based approach to deal with DES in the SCT framework. New formalization of DES as PCF along with auxiliary predicates, serving for accessibility of the automaton checking, simpli ed parallel composition construction. In future work predicates for controllable and observable events will be added to above PCFs for checking controllability, observability, etc., and designing supervisors. Although some results in this direction were obtained earlier, complex systems, built using the parallel composition, may be considered now due to the new results presented above.
Acknowledgments The research is supported by the Russian Science Foundation (project no. 16-11-00053). This work was also supported in part by the Presidium RAS, program no. 2, project "Methods and tools for solving hard-search problems with supercomputers" (reg. no. AAAA-A18118031590005-5).