=Paper=
{{Paper
|id=Vol-2430/paper3
|storemode=property
|title=PCF-based formalization of the parallel composition of automata
|pdfUrl=https://ceur-ws.org/Vol-2430/paper3.pdf
|volume=Vol-2430
|authors=Artem Davydov,Aleksandr Larionov,Nadezhda Nagul
|dblpUrl=https://dblp.org/rec/conf/iccs-de/DavydovLN19
}}
==PCF-based formalization of the parallel composition of automata==
https://ceur-ws.org/Vol-2430/paper3.pdf
PCF-based formalization of the parallel composition
of automata
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 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 different 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.
1. Introduction
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
finite state automata, sometimes called free behavior models and specifications. 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 specifications fulfillment.
In previous papers the application of automated theorem proving based on the positively-
constructed formulas (PCF) to the formalization of DES [1] was presented. The PCF calculus
advantages allow solving various problems of supervisor constructing sequence, for example,
problems of checking observability and co-observability of languages [2, 3].
The PCF calculus is developed in [4, 5] to formalize and solve some control theory problems.
In [5] the proof of soundness and completeness of the PCF calculus as the first-order logical
formalism is presented, and its further development may be found in [6]. The PCF calculus
is naturally aimed at solving problems of dynamic systems control due to its features, such
as modifiability of semantics (constructive, nonmonotonic, temporal, etc.) and an ability to
construct intuitionistic inferences of some non-Horn formulas. Constructive semantics allows
one to extract some knowledge (for example, action plans) from proofs, while non-monotonicity
and a treat of time 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 [5] with the examples of elevator group control, mobile robot action planning and
Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution
4.0 International (CC BY 4.0).
telescope guidance. Problems of automated theorem proving software in the PCF calculus design
and implementation are briefly discussed 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 each task being solved.
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 [8]
it is shown how state of the art problems of swarm robotics can be formalized and solved
using the SCT framework. Problems of segregation, aggregation, object clustering and group
formation are considered for two robotic platforms, the e-puck and the Kilobot. To formalize,
for example, the case study of segregation, four free behaviour models are used which represent
input device to configure the robot, the robot’s ability to assume one of the leader types or
to be a follower, motion capabilities, and the robot’s ability to receive messages from nearby
leader robots. Specification for the segregation case study consists of three automata: one of
them configures the robot through user interaction; one allows followers to move and leaders to
transmit a signal, and one moves the follower robot according to the signal received. To built a
supervisor, free behavior models and specifications are combined using an operation known as
parallel, or synchronous, composition.
In [9] to investigate the applicability of SCT to a high-tech system, a theme park vehicle,
called a multimover, is chosen. Its main structure contains mechanical parts to which sensors
and actuators are mounted. Supervisory control is used to coordinate the individual components
and give the desired functionality to the whole system. The user interface of the multimover
contains three buttons (the reset, the forward and the backward button) so three automata are
used to represent the buttons. Sensors of a multimover are modelled by six automata, with
five of them having the same structure. Two automata correspond to the steer motor and to
the drive motor. One automaton is employed for ride control and one for the scene program
handler. In the event-based framework, it is not possible to derive a centralized supervisor for a
problem of this size because parallel composition leads to state explosion phenomenon. However,
combining by parallel composition components effected by the same specification, aggregative
distributed synthesis [10] becomes possible.
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 specification language and helps to design supervisor
if specification occurs to be controllable. Target language [8], built as parallel composition of
the specification and the system automata, is a base for founding bad states which should be
forbidden by a supervisor.
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 PCF-
formalization of parallel composition is given in section 5. Application of the results obtained
are discussed in Conclusions.
2. Automata representation of discrete event systems
The first [11] and the most popular way to represent DES is a finite-state automaton. It is
defined as a structure G = (Q, Σ, δ, q0 , Qm ) where Q is the set of states q; Σ the set of events;
δ: Σ × Q → Q the transition function; q0 ∈ Q the initial state; Qm ⊂ Q the set of marker
states. Marked states correspond to some completed tasks performed by the system under
consideration, for example, finished processing sequence in manufacturing system. Note that
marking does not have any terminal meaning that is system proceeds after a marker state is
achieved. That is why G is called a generator of a formal language [11]. As usual, let Σ∗ denote
the set of all strings over Σ, including the empty string ε. δ is easily extended on strings from
Σ∗ . A language generated by G is L(G) = {w : w ∈ Σ∗ and δ(w, q0 )! }, while a language marked
by G is Lm (G) = {w : w ∈ L(G) and δ(w, q0 ) ∈ Qm }. Here δ(s, q0 )! means that δ(s, q0 ) is defined.
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.
Definition 1 [Parallel composition] If two generators Gi = (Qi , Σi , δi , q0i , Qim ), i = 1, 2, are
given then parallel composition is defined [12] as G1 ||G2 := Ac(Q1 × Q2 , Σ1 ∪ Σ2 , δ, (q01 , q02 ), Q1m ×
Q2m ),
(δ (σ, q 1 ), δ2 (σ, q 2 )) if δ1 (σ, q 1 )!, δ2 (σ, q 2 )!, and σ ∈ Σ1 ∩ Σ2 ,
1
(δ1 (σ, q 1 ), q 2 ) if δ1 (σ, q 1 )! and σ ∈ Σ1 \ Σ2 ,
δ(σ, q 1 , q 2 ) = (1)
(q 1 , δ2 (σ, q 2 )) if δ2 (σ, q 2 )! and σ ∈ Σ2 \ Σ1 ,
undefined otherwise.
Here Ac(G) denotes operation of taking accessible part of the automaton that is deleting all
states that are not reachable from q0 by some string from L(G) and transitions attached to these
states.
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
definition may be extended on any number of automata. Parallel composition is commutative
up to a reordering of the state components in composed states and associative: (G1 ||G2 )||G3 =
G1 ||(G2 ||G3 ). The parallel composition of a set of n automata can therefore be defined using
associativity: G1 ||G2 ||G3 := (G1 ||G2 )||G3 .
Example 1. Consider two state transition diagrams in figures 1 and 2. Initial states are
marked with arrows while double circles denote marked states. The automaton in figure 3 is the
result of the parallel composition of the automata in figures 1 and 2.
a b
a a
A B
b
b
c b X Y
a
C Figure 2. Generator G2 .
Figure 1. Generator G1 .
a
a
A,X B,Y
b
c b
C,X
Figure 3. The parallel composition of G1 and G2 .
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 undefined. In section 5 this example will be formalized by PCFs. Note that G2 may be
considered as a specification for G1 .
3. PCF calculus
Consider a language of a 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 a term, an atom, and a literal are defined in the usual way. Non-
atomic 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 = {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 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 },
respectively. 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 an empty disjunction is identical to f alse whereas an empty conjunction
is identical to true, the following equivalences are correct: ∀X A ∅ ≡ ∀X A → f alse ≡ ∀X A,
∃X A ∅ ≡ ∃X A&true ≡ ∃X A, ∀∅ Φ ≡ true → Φ ≡ ∀ Φ, and ∃∅ Φ ≡ true&Φ ≡ ∃ Φ.
The constructions ∀X A and ∃X A are called positive type quantifiers (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 n 6= z n ”. Originally, the term “type quantifier” was introduced by N. Bourbaki [13] as a
part of notation for formalization of mathematics.
3.1. PCF language explicit definition
Definition 2 [Positively constructed formula (PCF)] Let X be a set of variables and A a conjunct.
Then
(i) ∃X A and ∀X A are ∃–PCF and ∀–PCF, respectively.
(ii) If F = {F1 , . . . , Fn } is a set of ∀–PCFs then ∃X A : F is ∃–PCF.
(iii) If F = {F1 , . . . , Fn } is a set of ∃–PCFs then ∀X A : F is ∀–PCF.
(iv) Any ∃–PCF or ∀–PCF is PCF.
This form of logical formulas is referred to as positively constructed formulas (PCFs) as they
are written with positive type quantifiers 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 [5].
PCF starting with ∀∅ is called PCF in the canonical form. Any PCF can be represented
in the canonical form. If F is a non–canonical ∃–PCF then ∀∅ : F is the canonical PCF
since ∀∅ : F ≡ true → F ≡ F . If F is a non–canonical ∀–PCF then the canonical PCF is
∀∅ : {∃∅ : F } ≡ true → true&F ≡ F . Type quantifiers ∀∅ and ∃∅ are called fictitious since
they do not influence 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 quantifiers, and
we use corresponding names: node, root, leaf, branch. For example, PCF
∀ {∃X1 A1 {∀Y1 B1 , ∀B2 {∃X2 A2 , ∃A3 {∀Y2 B3 }, ∃A4 }}, ∃A5 {∀Y3 B4 }}
may be represented as a tree
∀Y1 B1
∃X1 A1 ∃X2 A2
∀B2 ∃A3 ∀Y2 B3
∀
∃A4
∃A5 ∀Y3 B4 .
Parts of a canonical PCF are named as follows:
(i) The root of a canonical PCF’s tree-view ∀∅ is called a PCF root.
(ii) Each PCF root child ∃X 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 ∀Y 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.
3.2. Inference rule
In the process of reasoning one often proves a statement F by refuting its negation. We intend
to proceed similarly.
Definition 3 [Answer] A question ∀Y D : Υ to a base ∃X A has an answer θ if and only if θ is
a substitution Y → H ∞ ∪ X and Dθ ⊆ A, where H ∞ is Herbrand universe based on constant
and function symbols that occur in corresponding base subformula.
Definition 4 [Splitting] Let B = ∃X A : Ψ, and Q = ∀Y D : Υ, where Υ =
{∃Z1 C1 : Γ1 , . . . , ∃Zn Cn : Γn } then split(B, Q) = {∃X∪Z1 0 A∪C1 0 : Ψ∪Γ1 0 , . . . , ∃X∪Zn 0 A∪Cn 0 : Ψ∪
Γn 0 }, where 0 is a variable renaming operator. We say that B is split by Q. Obviously,
split(B, ∀Y D) = split(B, ∀Y D : ∅) = ∅.
Definition 5 [Inference rule ω] Consider some canonical PCF F = ∀∅ : Φ. Let there exist
a question Q that has an answer θ to appropriate base B ∈ Φ. Then ωF = ∀∅ : Φ \ {B} ∪
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, ∀Y D) = ∅. The refuted base subformula B is removed from the set of base subformulas
Φ since Φ \ {S} ∪ ∅ = Φ \ {S}. Note that when the set Φ becomes empty after applying ω rule
and PCF becomes just ∀ then it can be concluded that the negation of the 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 a deduction of F in the PCF calculus (with the axiom ∀). Suppose that a search
strategy verifies the questions in consecutive order, without omissions (i.e. the verification 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).
Example 2. [Refutation of PCF] Consider PCF
∀x S(x) ∃A(x)
F1 = ∀ ∃S(e) ∀x, y C(x, y)
∃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 the only answer {x → e} to the first 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 :
∀x S(x) ∃A(x)
F2 = ∀ ∃S(e), A(e) ∀x, y C(x, y)
∃y C(y, f (x))
∀x A(x)
∃ ∀x S(x), A(x) ∃C(x, f (x))
At the second step there is also only one answer {x → e} to the question Q3 . After applying
ω with this answer, F2 is split because Q3 has the disjunctive branching. The formula gets the
form F3 :
Q1
∃y1 S(e), A(e), C(y1, f (e)) Q2
Q3
F3 = ∀ 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 to 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
second base which adds the atom C(e, f (e)) to it.
At the fifth step the only base can be refuted by answering to Q2 (the goal question) with
the answer {x → e; y → f (e)}. This finishes refutation because all the bases were refuted.
4. PCF features
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 quantifiers.
(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 ∃- and ∀-nodes which alternate
at each branch.
(iii) The negation of PCF is merely obtained by the replacement of the symbol ∃ with ∀, 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 [14] used, for example, in the resolution method [15]. Furthermore, it is
more compact than representations in terms of standard disjunctive and conjunctive normal
forms.
(v) It is not necessary to preprocess (scolemize) the formulas by eliminating of all existential
quantifiers. The scolemization procedure related to this elimination leads to elevating the
complexity of terms (see [14]).
(vi) The natural structure of the knowledge in the language of PCFs is retained better. Indeed,
the description of the knowledge in the original form does not employ ”theoretical”
quantifiers ∀x, ∃x. Instead of them, type quantifiers ∀x(A → t), ∃x(A&t) with simple and
natural forms of conditions A (e.g., without symbols ∀, ∃ inside of A) are employed. The
PCF structure retains most of the original structure of the knowledge when the knowledge
is written as an expression constructed of atoms (and/or their negations) with the help of
positive quantifiers and logic connectives &, ∨. In this case, the PCF structure may differ
from the initial structure merely by appending auxiliary quantifiers ∃∅ (instead of some
connectives &, ∨ mentioned above) and/or replacing the negations of atoms ¬A with the
structures ∀ A ∅.
Consider features (iv)–(vi) in greater detail with the help of the following example.
Example 3. The FOF
∀x(A& → (∃y1 B1& ∨ . . . ∨ ∃yk Bk& )), (2)
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
& (¬A1 ∨ . . . ∨ ¬Al ∨ Ci11 ∨ . . . ∨ Cikk ), (3)
(i1 ,...,ik )∈(1,n)k
i.e. contains (l + k)nk atoms (nk clauses). It is also obvious that, except of the auxiliary
quantifiers, 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:
∀X A {∃Y1 B1 , . . . , ∃Yk Bk }.
The language of clauses has been used in the resolution method [16] since its representation
(2) in comparison with formulas of the classical predicate calculus is hogeneous. This allowed J.
Robinson, basing on Herbrand’s results, to develop a popular method of automated deduction
with one inference rule known as the resolution rule.
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 specific 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 offers 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 specific
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 modified without any changes of the axiom ∀ and
the inference rule ω. Such modifications 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.
5. PCF formalization of parallel composition
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, first 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.
5.1. Formalization of a generator
Behavior of a generator, representing some DES, may be simulated using the logical inference
of a PCF which has the general structure depicted in figure 4.
∀σ, s, e, s0 L(σ, S), δ(s, e, s0 ) ∃L(σ · e, s0 )
∃ L(ε, S0 ), δ(S1 , e, S2 ), Lm (ε, S0 ), δm (S1 , e, S2 )
∀σ, s, e, s0 L(σ, S), δm (s, e, s0 ) ∃Lm (σ · e, s0 )
Figure 4. General view of PCF formalizing DES.
This way of formalization of a generator is more compact than the one previously suggested [1]
and gives more possibilities when setting up search strategies of the inference. Indeed, there is
the only base subformula describing the automaton. Transitions of the automaton are listed in
the base of facts and two questions correspond to the implementation of transitions, with one
of them corresponding to marked transitions. If an answer to a question is found, L(. . . , . . .)
or Lm (. . . , . . .) atoms are added to the base, with a new event as the first argument, thus
accumulating strings of the generated and marked languages.
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),
(G1P CF )
Lm (ε, A), δm (A, a, A), δm (A, b, B), δm (B, a, A), δm (B, b, B), δm (C, b, B).
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 figure 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),
(G2P CF )
δm (X, b, Y ).
Table 1 describes the inference of PCF with the base G2P CF . The first 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 first 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: Inference of PCF for G2 .
Q Base atoms Substitution Atoms added
1 δ(X, b, Y ) {σ → ε, s → X, e → b, s0 → Y } L(b, Y )
Continued on the next page
Table 1 – continued from the previous page
Q Base atoms Substitution Atoms added
2 0
δm (X, b, Y ) {σ → ε, s → X, e → b, s → Y } Lm (b, Y )
1 δ(X, a, X) {σ → ε, s → X, e → a, s0 → X} L(a, X)
1 δ(Y, a, X) {σ → b, s → Y, e → a, s0 → X} L(ba, X)
2 δm (X, b, y) {σ → a, s → X, e → b, s0 → Y } Lm (ab, Y )
1 δ(X, b, y) {σ → ba, s → X, e → b, s0 → Y } L(bab, Y )
2 δm (X, b, y) {σ → ba, s → X, e → b, s0 → Y } Lm (bab, Y )
1 δ(X, a, X) {σ → ba, s → X, e → b, s0 → X} L(baa, X)
and so on...
5.2. Formalization of parallel composition
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 figure 4, representing some generators G1 and G2 . To separate different automata in the
combined base, atoms are indexed with the numbers of PCFs. To obtain PCF representing
G1 ||G2 , we combine bases and questions of F1 and F2 , and add new questions that represent the
rules of (1) in definition 1 (section 2). PCF in figure 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 G1 ||G2 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 first 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
first 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 \ Σ2 , and Σ2 \ Σ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 finite 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 figure
5 can be used to obtain languages for the constructed composition, if we add a pair of questions
similar to the first 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 figure 5. The inference with the corresponding
composition automaton drawing is depicted in table 2.
∀σ, s, e, s0 L1 (σ, S), δ 1 (s, e, s0 ) ∃L1 (σ · e, s0 )
∀σ, s, e, s0 L1 (σ, S), δm
1 (s, e, s0 ) ∃L1m (σ · e, s0 )
∀σ, s, e, s0 L2 (σ, S), δ 2 (s, e, s0 ) ∃L2 (σ · e, s0 )
∀σ, s, e, s0 L2 (σ, S), δm
2 (s, e, s0 ) ∃L2m (σ · e, s0 )
∀s, p L1 (ε, s), L2 (ε, p) ∃L3 (ε, sp)
∃ L1 (ε, S0 ), ∀s, p L1 (ε, s), L2 (ε, p) ∃δ 3 (ε, ε, sp)
L1m (ε, S0 ),
∀σ, s1 , p1 , s2 , p2 δ 1 (s1 , σ, s2 ), δ 2 (p1 , σ, p2 ),
L2 (ε, S0 ), ∃δ 3 (s1 p1 , σ, s2 p2 )
δ i ( , , s1 p1 )
L2m (ε, S0 ),
δ 1 (S1 , e, S2 ), 1 (s , σ, s ), δ 2 (p , σ, p ),
∀σ, s1 , p1 , s2 , p2 δm 1 2 m 1 2 3 (s p , σ, s p )
1 (S , e, S ),
δm i ( , ,s p ) ∃δm 1 1 2 2
1 2 δm 1 1
δ 2 (S1 , e, S2 ),
δm2 (S , e, S ) ∀σ, s1 , p1 , s2 , p2 δ 1 (s1 , σ, s2 ), σ ∈ Σ1 , σ ∈ / Σ2 ,
1 2 ∃δ 3 (s1 p1 , σ, s2 p1 )
δ i ( , , s1 p1 )
1 (s , σ, s ), σ ∈ Σ , σ ∈
∀σ, s1 , p1 , s2 , p2 δm / Σ2 ,
1 2 1 3 (s p , σ, s p )
i ( , ,s p ) ∃δm 1 1 2 1
δm 1 1
∀σ, s1 , p1 , s2 , p2 δ 2 (p1 , σ, p2 ), σ ∈
/ Σ1 , σ ∈ Σ2 ,
∃δ 3 (s1 p1 , σ, s1 p2 )
δ i ( , , s1 p1 )
2 (p , σ, p ), σ ∈
∀σ, s1 , p1 , s2 , p2 δm / Σ1 , σ ∈ Σ2 ,
1 2 3 (s p , σ, s p )
i ( , ,s p ) ∃δm 1 1 1 2
δm 1 1
Figure 5. General view of PCF constructing parallel composition of two automata.
Table 2: Inference of PCF constructing G1 ||G2 .
Q Base atoms Substitution Atoms added Result
5 L1 (ε, A), L2 (ε, X) {s → A, p → X} L(ε, AX) A,X
6 L1 (ε, A), L2 (ε, X) {s → A, p → X} δ 3 (ε, ε, AX) A,X
7 δ 3 (ε, ε, AX), {s1 → A, p1 → δ 3 (AX, a, AX)
δ 1 (A, a, A), X, σ → b, s2 →
δ 2 (X, a, X) A, p2 → X}
7 δ 1 (A, b, B), {s1 → A, p1 → δ 3 (AX, b, BY )
δ 2 (X, b, Y ) X, σ → b, s2 →
B, p2 → Y }
Continued on the next page
Table 2 – continued from the previous page
Q Base atoms Substitution Atoms added Result
8 1 (A, b, B),
δm {s1 → A, p1 → 3 (AX, b, BY )
δm
2 (X, b, Y )
δm X, σ → b, s2 →
B, p2 → Y }
9 δ 3 (ε, ε, AX), {s1 → A, p1 → X, δ 3 (AX, c, CX)
δ 1 (A, c, C) σ → c, s2 → C}
7 δ 3 (AX, b, BY ), {s1 → B, p1 → δ 3 (BY, a, AX)
δ 1 (B, a, A), Y, σ → a, s2 →
δ 2 (Y, a, X) A, p2 → X}
7 δ 3 (AX, c, CX), {s1 → C, p1 → δ 3 (CX, b, BY )
δ 1 (C, b, B), X, σ → b, s2 →
δ 2 (X, b, Y ) B, p2 → Y }
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 {1, 2, 3} and the symbols “ ” correspond to variables, i.e. placements for the
substitution of any terms.
6. Conclusions
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, simplified 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-A18-
118031590005-5).
References
[1] Davydov A, Larionov A and Nagul N 2017 2017 40th International Convention on Information and
Communication Technology, Electronics and Microelectronics (MIPRO) (IEEE)
[2] Davydov A, Larionov A and Nagul N 2018 2018 41st International Convention on Information and
Communication Technology, Electronics and Microelectronics (MIPRO) pp 0938–0943
[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] Vassilyev S N 1990 The Journal of Logic Programming 9 235–266
[5] Zherlov A K, Vassilyev S N, Fedosov E A and Fedunov B E 2000 Intelligent control of dynamic systems
(Moscow: Fizmatlit) in Russian
[6] Davydov A, Larionov A and Cherkashin E 2011 Automatic Control and Computer Sciences 45 402–407
[7] Larionov A, Davydov A and Cherkashin E 2013 International Convention on Information and
Communication Technology, Electronics and Microelectronics (MIPRO), Opatija 2013 1023–1028
[8] Lopes Y K, Trenkwalder S M, Leal A B, Dodd T J and Groß R 2016 Swarm Intelligence 10 65–97 ISSN
1935-3820 URL http://dx.doi.org/10.1007/s11721-016-0119-0
[9] Forschelen S T J, van de Mortel-Fronczak J M, Su R and Rooda J E 2012 Discrete Event Dynamic Systems
22 511–540 ISSN 1573-7594 URL http://dx.doi.org/10.1007/s10626-012-0130-6
[10] Su R, van Schuppen J H and Rooda J E 2010 IEEE Transactions on Automatic Control 55 1627–1640 ISSN
0018-9286
[11] Ramadge P J and Wonham W M 1987 SIAM Journal on Control and Optimization 25 206–230
[12] Cassandras C G and Lafortune S 2008 Introduction to Discrete Event Systems (Springer US)
[13] Bourbaki N 2004 Theory of sets (Springer Berlin Heidelberg)
[14] Davis M and Putnam H 1960 J. ACM 7 201–215 ISSN 0004-5411 URL
http://doi.acm.org/10.1145/321033.321034
[15] Robinson J A 1965 J. ACM 12 23–41 ISSN 0004-5411 URL http://doi.acm.org/10.1145/321250.321253
[16] Russell S and Norvig P 2010 Artificial Intelligence: A Modern Approach 3rd ed Series in Artificial Intelligence
(Upper Saddle River, NJ: Prentice Hall) URL http://aima.cs.berkeley.edu/