A graph model of message passing processes
Andrew M. Mironov
TL;DR
This paper introduces a graph-based model for message passing processes and presents a verification method, demonstrated through the example of verifying a sliding window protocol.
Contribution
It proposes a novel graph model for message passing and a verification method, applied to a specific protocol example.
Findings
Successful verification of the sliding window protocol
The graph model effectively captures message passing behaviors
The method provides a systematic approach for process verification
Abstract
In the paper we consider a graph model of message passing processes and present a method verification of message passing processes. The method is illustrated by an example of a verification of sliding window protocol.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Embedded Systems Design Techniques · Petri Nets in System Modeling
11institutetext: Moscow State University
A graph model of message passing processes
Andrew M. Mironov
Abstract
In the paper we consider a graph model of message passing processes and present a method verification of message passing processes. The method is illustrated by an example of a verification of sliding window protocol.
Keywords:
graph model, message passing processes, verification
1 Introduction
The problem of formal representation and verification of discrete processes is one of the most important problems in computer science. There are several approaches to this problem, the main of them are: CCS and -calculus [1], [2], CSP and its generalizations [3], temporal logic and model checking [4], Petri nets [5], process algebras [6], communicating finite-state machines [7].
In the present paper we introduce a new model of discrete processes, which is a synthesis of Milner’s model of processes [1] and the model of communicating finite-state machines [7]. Discrete processes are represented in our model as graphs, edges of which are labelled by operators. These operators consist of internal actions and communication actions. Proofs of correctness of processes are represented by sets of formulas, associated with pairs of states of analyzed processes. This method of verification of processes is a synthesis of Milner’s approach related on the concept of an observational equivalence [1] and Floyd’s inductive assertion method [8]. For a simplification of an analysis of processes we introduce a simplification operation on processes. With use this operation it is possible to reduce a complexity of verification of processes. We illustrate an advantage of the proposed model and the verification method on the example of verification of a two-way sliding window protocol.
2 Motivation, advantages of the proposed approach and
its comparison with other works
2.1 Motivation of the proposed approach
The main disadvantage of modern methods of verification of discrete processe is their large complexity. More precisely,
- •
the main disadvantage of verification methods based on model checking approach is a high computational complexity related to the state explosion problem, and
- •
disadvantages of methods based on theorem proving approach are related with a high complexity of construction of corresponging theorems and their proofs, and also with an understanding of these proofs.
For example, in recent paper [9] a complete presentation of proofs of theorems related to verification of two-way sliding window protocol takes a few dozen pages of a complex mathematical text.
The main motivation for the proposed approach to modeling and verification of discrete systems by checking of observational equivalence of corresponded message passing processes is to simplify and make more obvious the following aspects of modeling and analysis of discrete systems: representation of mathematical models of analyzed systems, construction of proofs of correctness of the systems, and understanding of these proofs by any who is not a strong expert in the mathematical theory of verification of discrete systems.
2.2 Advantages of the proposed approach
The proposed mathematical model of message passing processes with allows to construct such mathematical models of analysed systems that are very similar to an original description of these systems on any imperative programming language. In section 9 we give an example of such model that corresponds to a C-program describing a sliding window protocol using go back (the program was taken from book [10], section 3.4.2).
The main advantage of the proposed approach is a possibility to use a simplification operation of models of analyzed systems, that allows essentially simplify the problem of verification of these models. In section 9 we present a result of such simplification for the above model of a sliding window protocol: this model can be simplified to a model with only one state. It should be noted also that the simplified models allow more clearly understand main features of analyzed systems, and facilitate a construction of correctness proofs for analyzed systems.
If an analyzed property of a system has the form of a behavior which is described by some process, for example, in the case when
- •
an analyzed system is a network protocol, and
- •
a property of this system is a description of an external behavior of this protocol (related to its interaction with a higher-level protocol)
then a proof of a correctness of such system in this model is a set of formulas associated with pairs of states, the first of which is a state of the analyzed system, and the second is a state of a a process which describes a property of the analyzed system.
In section 9 we give an example of such proof, which is a small set of simple formulas. These formulas can be naturally derived from a simplified model of an analyzed protocol.
Another advantage of the proposed approach is a possibility to verify systems with unbounded sets of states. One of examples of such systems is the above sliding window protocol using go back .
2.3 Comparison with other works
In this section we present an overview of papers related to verification of message passing systems, which are most relevant to the present paper.
The paper [9] deals with modeling and manual verification in the process algebraic language CRL. Authors use the theorem prover PVS to formalize and to mechanically prove the correctness of a protocol using selective repeat (a C-program describing this protocol is presented in section 3.4.3 of the book [10]). The main disadvantage of this work is a large complexity of proofs of theorems related to verification of this protocol. This protocol can be verified more simply with use of the approach proposed in the present paper.
There are a lot of works related to verification of systems with message passing based on temporal logic and model checking approach. Most relevant ones to the present paper are [11], [12], [13], [14], [15], [16], [17]. The most deficiency of all of them is restricted abilities: these methods allow verify only finite state systems.
Among other approaches it should be noted approaches with use of first order logic and assertional verification: [18], [19], and approaches with use of process algebra: [20]. The most deficiency of these approaches is a high complexity of construction of proofs of correctness of analyzed systems.
3 Auxiliary concepts
3.1 Terms
We assume that there are given a set of variables, a set of values, a set of constants, and a set of function symbols. Any constant from is interpreted by a value from , and any function symbol from is interpreted by an operation on .
We assume that contains constants 0 and 1, and contains boolean function symbols , which correspond to standard boolean operations on .
The set of terms is defined in the standard way. Variables and constants are terms. Other terms have the form , where , and are terms. For each a set of all variables occurring in is denoted by .
If , then a valuation of variables of is a correspondence , that associates each variable with a value . We denote by the record the set of all valuations of variables from . For each , each and each the record denotes an object called a value of on and defined in the standard way. We assume that terms and are equal iff .
A term is a formula if the value is 0 or 1. The set of all formulas is denoted by . The symbols and denote true and false formula respectively. We shall write formulas of the form , , etc. in a more familiar form , , etc.
3.2 Atomic operators
We assume that there is given a set , whose elements are considered as names of objects that can be sent or received by processes.
An atomic operator (AO) is an object of one of three forms presented below. Each pair (), where is an AO, and is a valuation of variables occurred in , corresponds to an action , informally defined below.
An input is an AO of the form , where and . An action is a receiving from another process an object named , with a message attached to this object, this message is assigned to the variable . 2. 2.
An **output ** is an AO of the form , where and . An action is a sending to another process an object named , to which a message is attached. 3. 3.
An assignment is an AO of the form , where , . An action is an assigning the variable with the value .
Below we use the following notations.
- •
For each AO the record denotes the set of all variables occurred in .
- •
If , and is an assignment, then the record denotes a term defined as follows: let has the form , then is obtained from by a replacement of all occurrences of the variable by the term .
- •
If is an assignment, and , where , then the record denotes a valuation from , defined as follows: let , then and .
It is easy to prove that if is an assignment and , then for each , where , the equality holds. This equality is proved by an induction on the structure of the term .
3.3 Operators
An operator is a record of the form , where is a formula called a precondition of (this formula will be denoted as ), and is a sequence of AOs (this sequence will be denoted as ), among which there is at most one input or output. The sequence may be empty ().
If contains an input (or an output) then is called an input operator (or an output operator), and in this case the record denotes a name occurred in . If does not contain inputs and outputs, then we call an internal operator.
If , then such precondition can be omitted in a notation of .
Below we use the following notations.
For each operator a set of all variables occurred in is denoted by . 2. 2.
If is an operator, and , then the record denotes an object, which either is a formula or is not defined. This object is defined recursively as follows. If empty, then . If , where , then we shall denote by the record an operator obtained from by a removing of its last AO, and
- •
if , then , if , and is undefined otherwise
- •
if , then
- •
if , then . 3. 3.
If is an internal operator, and , where , then the record denotes a valuation from , defined as follows: if is empty, then , and if , where , then .
It is easy to prove that if is internal and , then for each , where , such that , the equality holds. This equality is proved by an induction on a lenght of .
3.4 Concatenation of operators
Let and be operators, and at least one of them is internal.
A concatenation of and is an object denoted by the record , that either is operator or is undefined. This object is defined iff is defined, and in this case . It is easy to prove that
- •
if operators and formula are such that objects in both sides of the equality are defined, then this equality holds, and
- •
if operators are such that all objects in both sides of the equality are defined, then this equality holds.
4 Message passing
processes
4.1 A concept of a message passing process
A message passing process (also called more briefly a process) is a graph of the form
[TABLE]
components of which have the following meanings.
- •
is a set of nodes of , which are called states of the process .
- •
is an initial state of the process .
- •
is a set of edges of the graph , which are called transitions, each transition from has the form , where , and is an operator, which is a label of this edge.
- •
is a precondition of the process .
A transition is called an input, an output, or an internal transition, if is an input operator, an output operator, or an internal operator, respectively.
For each process
- •
the record denotes the set consisting of
- –
all variables occurred in any of the transitions from , or in , and
- –
a variable , which is not occurred in , and in transitions from , the set of values of is
- •
the record denotes the formula .
For each transition the records , , and denote an operator, a formula and states defined as follows: if has the from , then
[TABLE]
If is an input or an output, then the record denotes the name .
A set of essential variables of is a smallest (w.r.t. inclusion) set satisfying the following conditions.
- •
contains all variables contained in preconditions and outputs in operators , where .
- •
If contains an AO and , then contains all variables occurred in .
4.2 Actions of processes
An **action of a process ** (or, briefly, an action) is a record of one of the following three forms.
- •
, where and . An action of this form is called a receiving of an object named with the attached message .
- •
, where and . An action of this form is called a sending of an object named with the attached message .
- •
. An action of this form is called a silent action.
A set of all actions is denoted by .
4.3 An execution of a process
An execution of a process (1) is a walk on the graph starting from , with an execution of AOs occurred in labels of traversed edges. At each step of this walk there is defined a current state and a current valuation . We assume that , , and for each step of this walk .
An execution of on step is described informally as follows. If there is no transitions in starting at , then terminates, otherwise
- •
selects a transition , such that , and if is an input or an output, then at the current moment can receive or send respectively an object named (i.e. at the same moment there is another process that can send to or receive from respectively an object named ). If there is no such transition, then suspends until at least one such transition will appear, and after resumption its execution selects one of such transitions,
- •
after a sequential execution of all AOs occurred in the operator of the selected transition , moves to the state .
An execution of each AO occurred in consists of a performing of an action and a replacement the current valuation on a valuation , which is considered as a current valuation after an execution of the AO . An execution of an AO is as follows:
- •
if , then performs an action of the form , and ,
- •
if , then performs the action , and
- •
if , then performs , and , .
5 Operations on processes
In this section we define some operations on processes which can be used for a construction of complex processes from simpler ones. These operations are generalizations of corresponded operations on processes defined in Milners’s Calculus of Communicating Systems [1].
5.1 Parallel composition
The operation of parallel composition is used for building processes, composed of several communicating subprocesses.
Let be processes, such that and . A parallel composition of and is a process , where , , , and consists of the following transitions:
- •
for each transition of the process , and each state of the process has the transition
- •
for each transition of the process , and each state of the process the process has the transition
- •
for each pair of transition of the form \left\{\begin{array}[]{llllllllllllll}s_{1}\;\mathop{\to}\limits^{O_{1}}\;s^{\prime}_{1}\;\in T_{P_{1}}\\ s_{2}\;\mathop{\to}\limits^{O_{2}}\;s^{\prime}_{2}\;\in T_{P_{2}}\end{array}\right. where one of the operators , has the form , and another operator has the form , the process has the transition , where and [O]=\Big{(}(O^{\prime}_{1}\cdot O^{\prime}_{2})\cdot[x:=e]\Big{)}\cdot(O^{\prime\prime}_{1}\cdot O^{\prime\prime}_{2}).
A parallel composition of and is denoted by the record .
If or , then before a construction of the process it is necessary to replace states and variables occuring in both processes on new states or variables respectively.
For any tuple of processes their parallel composition is defined as the process .
5.2 Restriction
Let be a process, and be a subset of the set .
A restriction of with respect to is the process which is obtained from by removing of those transitions that have labels with the names from , i.e. T^{\prime}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\left\{\begin{array}[]{llllllllllllll}({\matrix{s&\begin{picture}(20.0,8.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle O}} \end{picture}&s^{\prime}}})\in R\left|\begin{array}[]{llllllllllllll}[O]=[\;],\;\;\mbox{or}\;N_{O}\not\in L\end{array}\right\}\end{array}\right..
5.3 Renaming
The last operation is called a renaming: for any mapping and any process the record denotes a process which is called a renaming of and is obtained from by changing of names occurred in : any name occurred in is changed on .
If the mapping acts non-identically only on the names , and maps them to the names respectively, then the process can be denoted also as .
6 Realizations of processes
6.1 Realizations of AOs and
sequences of AOs
A realization of an AO is a triple , such that
- •
, where , and
- •
if , then and
- •
if , then and
- •
if , then and .
Let be a sequence of AOs which contains at most one input or output. A realization of is a triple , such that
- •
, where and
- •
if , then and , otherwise there exists a sequence
[TABLE]
where , , is a realization of , and , if each in (2) is equal to , otherwise coincides with that , which is different from .
6.2 Realization of transitions
Let be a process of the form (1), and .
A realization of is a triple , where and , such that and is a realization of .
The following properties hold.
- •
If a transition is internal or is an output, then for each , such that , there exist a unique and a unique , such that is a realization of . We shall denote such by .
- •
If a transition is an input, then for each , such that , and each there exists a unique , such that is a realization of . We shall denote such by .
6.3 Realizations of processes
A realization of a process is a graph having the following components.
- •
The set of vertices of is the disjoint union .
- •
The set of edges of consists of the following edges:
- –
for each realization of any the graph has an edge from to with a label , and
- –
for each , such that , and each edge of from to with a label the graph has an edge from to with a label .
We shall use the following notations: for any pair of vertices of
- •
the record denotes an edge from to with a label
- •
means that either or the graph has an edge , and , .
- •
(where ) means that the graph has an edge , and , .
7 Observational equivalence of processes
7.1 A concept of observational equivalence of processes
Processes and are said to be observationally equivalent if and are observationally equivalent in Milner’s sense [1], i.e. there exists , such that
2. 2.
if and , then ,
if and , then 3. 3.
if and , , then ,
if and , , then
The record means that and are observationally equivalent.
A lot of problems related to verification of discrete systems can be reduced to the problem to prove that , where the process is a model of a system being analyzed, and is a model of some property of this system. In section 9 we consider an example of a proof that , where is a model of the sliding window protocol, and is a model of its external behavior.
7.2 A method of a proof of observational
equivalence of processes
In this section we present a method of a proof of observational equivalence of processes. This method is based on theorem 7.2. To formulate and prove this theorem, we introduce auxiliary concepts and notations.
Let be a process, and . A composite transition (CT) from to is a sequence of transitions of of the form
[TABLE]
such that there is at most one input or output operator among , and there are defined all concatenations in the expression
[TABLE]
Sequence (3) may be empty, in this case . If CT is not empty and has the form (3), then the record denotes a value of the expression (4). If CT is empty, then .
We shall use for CTs the same concepts and notation as for ordinary transitions (, , etc.). A CT is said to be an input, an output, or an internal iff is an input operator, an output operator, or an internal operator, respectively.
A concept of a realization of a CT is defined by analogy with the concept of a realization of a transition (see section 6.2). This concept has properties similar to properties of a realization of a transition, in particular:
- (a)
if a CT is internal or is an output, then for each , such that , there is a unique and a unique , such that is a realization of , we shall denote such by the record 2. (b)
if a CT is an input, then for each , such that , and each there is a unique , such that is a realization of , we shall denote such by the record . 2. 2.
If and are formulas, then the record is a brief notation of the proposition that the formula is true. 3. 3.
If are operators, and , then the record denotes a formula defined by a recursive definition presented below. In this definition we use records of the form and , which denote an operator and a formula respectively, defined in section 3.3.
Let and , then the formula
[TABLE]
is defined as follows:
- (a)
, if 2. (b)
, if is an assignment 3. (c)
, if is an assignment 4. (d)
, if , and is a formula obtained from replacing all occurrences of and on a fresh variable (i.e. is not occurred in , and ) 5. (e)
, if and 6. (f)
, otherwise.
Theorem 1
Let be processes such that and . Then , if there exist a set of formulas with variables from , such that
2. 2.
there exists a set of CTs of such that 3. 3.
there exists a set of CTs of such that
8 Simplification of processes
8.1 A concept of a simplification of processes
The concept of a simplification of processes is intended to reduce the problem of verification of processes.
A simplification of a process is a sequence of transformations of this process, each of which is performed according to one of the rules set out below. Each of these transformations (except the first) is performed on the result of previous transformation. A result of a simplification is a result of last of these transformations.
Simplification rules are defined as follows. Let be a process.
Rule 1 (removing of states).
If , and
- •
, , are all transitions incoming to
- •
, , are all transitions outgoing from , and if all these transitions are internal, then if
- •
- •
then and all transitions related to are removed from , and the transitions (where ) are added to .
Rule 2 (fusion).
If has a pair of transitions of the form , , and , then this pair is replaced by a transition , where .
Rule 3 (elimination of unessential assignments).
If has an AO , where , then this AO is removed from .
Theorem 1. If is a result of simplification of , then .
9 An example: verification of a
sliding window protocol
In this section we present an example of use of theorem 7.2 for a verification of a sliding window protocol. This protocol ensures a transmission of messages from one agent to another through a medium, in which messages may get distorted or lost. In this section we consider a two-way sliding window protocol, in which the agents can both send and receive messages from each other. We do not present here a detail explanation of this protocol, a reader can find it in section 3.4.2 of the book [10] (a protocol using go back ).
9.1 A structure of the protocol
The protocol is a system consisting of interacting components, including
- •
components that perform a formation, sending, receiving and processing of messages (such components are called agents, and messages sent from one agent to another, are called frames), and
- •
a medium, through which frames are forwarded (such a medium is called a channel).
A detailed description of the components and relation between them is represented in the Appendix.
9.2 Specification
External actions of the above protocol (i.e. actions which are related to its communication with a network level) have the form , , and . Assume that we take into account only external actions and , and ignore other its external actions (i.e. we consider a transmission only in one direction: from the left to the right). We would like to prove that such behavior is equivalent to a behavior of a process , which is called “a FIFO buffer which can hold at most frames”, and is defined as follows:
- •
variables of are
- –
an array , elements of which have the same type as a type of frames in the above protocol, and
- –
variables , values of which belong to , and have the following meaning: at every moment
a value of is equal to a number of frames in the buffer
- *
values and can be interpreted as lower and upper bounds of a part of the array , which stores the received frames, which has not yet been issued from the buffer
- •
has one state and 2 transitions with labels
[TABLE]
where and
- •
initial condition is .
A process that describes a behavior of the protocol with respect to the above specific point of view (where we ignore actions of the form and ) is constructed as a parallel composition of the processes corresponded to components of this procotol, with elimination of atomic operators related to ignored communications.
9.3 Verification
With use of the simplification operations from section 8, we can transform the process corresponded to the protocol (with elimination of atomic operators which are corresponded to ignored actions) to a process with only one state and with transitions labelled by the following operators:
- •
- •
- •
, where , if , and , otherwise
- •
- •
- •
- •
where dots denote unessential components of expressions, and the symbols , , , and have the following sense:
- •
and are variables of the process , and values of these variables are lists of frames which were received by the process ( holds frames received from ), every received frame is added to the end of a corresponded list
- •
is an expression, a value of which is equal to the first element of the list
- •
is an expression, a value of which is equal to the list without its first element
- •
is a function of an addition of a frame to the end of a list
- •
is a constant, a value of which is an empty list.
For a proof that the process is observationally equivalent to the process , we define a formula where is a unique state of and is a unique state of as a conjunction of the following formulas:
- •
- •
- •
- •
- •
- •
- •
if a value of is , then the sequence is monotonically increasing (mod ) subsequence of
(the last record is not a formula, but can be represented by a formula, we omit this representation).
It is not so diffcult to check that satisfies the conditions of theorem 7.2 and this proves that the process is observationally equivalent to .
10 Conclusion
The concept of a process with message passing which is presented in this paper can be considered as a formal model of a communicating program without recursion. In the paper we have established suffcient conditions of observational equivalence of processes. The next steps of investigations in this area can be the following: find necessary and suffcient conditions of observational equivalence of message passing processes, generalize the proposed concept of a process with message passing for formal modeling of communicating programs with recursion, and find necessary and suffcient conditions of observational equivalence of such processes.
Appendix
11 A description of
sliding window protocol
11.1 Frames
Each frame , which is sent by any of the agents, contains a packet , and a couple of numbers:
- •
a number (where is a fixed integer), which is associated with the packet and with the frame , and
- •
a number , which is a number associated with a last received undistorted frame.
To build a frame, a function is used, i.e. a frame has the form .
To extract the components , , from the frame , the functions , and are used, these functions have the following properties:
[TABLE]
11.2 Window
The set of variables of an agent contains an array . Values of some components of this array are packets which are sent, but not yet acknowledged. A set of components of the array , which contain such packets at a current time, is called a window.
Three variables of the agent are related to the window: (a lower bound of the window), (an upper bound of the window), and (a number of packets in the window). Values of these variables belong to the set . At the initial moment values of , and are equal to 0. At any moment the window can be empty (if ), or not empty (if ). In the last case the window consists of elements of with indices from the set , where denotes the set
- •
, if , and
- •
, if .
Adding a new packet to the window is performed by an execution of the following actions: this packet is written in the component , is increased by 1 modulo (i.e. a new value of is assumed to be , if , and 0, if ), and is increased by 1. Removing a packet from the window is performed by an execution of the following operations: is increased by 1 modulo , and is decreased by 1 (i.e. it is removed a packet whose number is equal to the lower bound of the window).
If an agent received a frame, the third component of which (i.e. a number of an acknowledgment) is such that , then all packets in the window with numbers from are considered as acknowledged and are removed from the window (even if their acknowledgments were not received).
11.3 Flow graph
A relation between subprocesses of sliding window protocol is represented by the flow graph:
[TABLE]
[TABLE]
11.4 Timers
Each component of the array is associated with a timer, which determines a duration of waiting of an acknowledgement from another agent of a receiving of the packet contained in the component . The combination of these timers is considered as a process , which has an array of boolean variables. The process has one state and transitions which are labeled by the following operators:
- •
- •
- •
(where )
An initial condition is .
If an agent has received an object with a name from a timer, then the agent sends again all packets from its window.
11.5 Agents
A behavior of each agent is described by the same process, combining functions of a sender and a receiver. This behavior can be represented by the following flowchart.
[TABLE]
where
- •
is an abbreviation of the list of AOs \left\{\begin{array}[]{lllll}C\,!\,\varphi(x[s],s,r\mathop{-}\limits_{n}1)\\ start\;!\;s\\ s:=s\mathop{+}\limits_{n}1\end{array}\right\}
- •
is a special notation for a distorted message, and
- •
a value of the variable is 1, if the agent can receive a new packet from his network level (i.e. ), and 0, otherwise.
Processes and are obtained by a simple transformation of this flowchart, and by an addition of corresponded index (1 or 2) to its variables and names.
11.6 A proof of theorem 1
Since , then there is a natural bijection between and . Below we identify these two sets.
We define the relation as follows:
[TABLE]
We prove that satisfies the conditions from section 7.1.
The condition follows from the definition of . 2. 2.
Let and . We must prove that
[TABLE]
We consider separately the cases and .
If , then , and according to definition of the graph (section 6.3), and the graph has the edge , i.e. is a realization of a transition from , where is an internal operator.
According to item 2 in the theorem, there exists a set of CTs of process , such that
[TABLE]
Since , then : , so
[TABLE]
(the last inequality holds according to property 1 in the statement of the theorem).
According to the definition of a realization of a transition, the equality holds. This equality, (7) and (8), imply that there is such that
[TABLE]
It is easy to prove that the equality
[TABLE]
holds. This equality is an analogue of the equality in the end of section 3.3, and is proved by induction on the total number of AOs in and .
[TABLE]
By the definition of and , the statement (6) in this case () follows from the statement
[TABLE]
Define . Since , and , then (12) follows from the statements
[TABLE]
[TABLE]
(13) follows from the definitions of concepts of a CT and a concatenation of operators and from the statements and . The first of these statements follows from the equality , and the second is justified as follows. The definition of formulas of the form implies that the statement (9) can be rewritten as
[TABLE]
where is some formula. Since , then (15) implies the desired statement .
(14) follows from (11) and from the assumption that and do not occur in , and .
Thus, in the case the property (6) holds.
In the case the property (6) can be proved similarly. 3. 3.
Let and , where . We must prove that
[TABLE]
- (a)
At first consider the case and .
If , then , and according to the definition of the graph (section 6.3), and the graph has the edge , i.e. is a realization of a transition of the form from , where is an input operator. Using the notation introduced at the end of section 6.2, we can write .
Just as in the preceding item, we prove that : , and there exists a CT of the process , such that the equality
[TABLE]
holds, which should be understood in the following sense: for each of valuation (where is a variable, referred in the item 3d of the definition from section 7.2, we can assume that ), coinciding with on , the equality \Big{(}(O_{1},O_{T_{i}})\cdot b_{s^{\prime}_{1}s^{i}_{2}}\Big{)}^{\xi}=1 holds. In particular, (17) implies that is an input operator, and .
Define . It is easy to prove that , and the statement (16) in the case follows from the equality
[TABLE]
which is justified as follows.
In this case and can be represented as concatenation of the form
[TABLE]
Definition of formulas of the form (5) implies that
[TABLE]
(17) and (19) imply the equality
[TABLE]
Its special case is the equality
[TABLE]
The last equality can be rewritten as
[TABLE]
whence it follows that
[TABLE]
It is easy to see that the left side of (20) coincides with the left side of the equality (18).
Thus, in the case and the property (16) is proven.
In the case and the property (16) can be proved similarly. 2. (b)
Now we prove (16), when . As in the previous item, we consider only the case .
If , then , and
- •
and the graph has the edge , i.e. is a realization of a transition of the form , where is an output operator
- •
: , and there exists a CT of the process , such that
[TABLE]
(21) implies that is an output operator, and .
Define . For a proof of (16) it is enough to prove the statements
[TABLE]
[TABLE]
In this case and can be represented as concatenations of the form
[TABLE]
[TABLE]
The definition of formulas of the form (5) implies that
[TABLE]
(21) and (26) imply the equality
[TABLE]
from which it follows that
[TABLE]
[TABLE]
By assumption, is a realization of the transition . From the representation of as a concatenation (24) it follows that , whence, according to (27) we get the equality . From this and from a representation of as a concatenation (25) it follows that is a realization of the CT . Since and , then it follows that we are justified the statement (22).
The statement (23) follows from (28).
Thus, in the case and the property (16) is proven.
In the case and the property (16) can be proved similarly
The symmetrical conditions on the relation (i.e., second parts of the conditions on , presented in second and third items in section 7.1) can be proved similarly.
12 An example of a process defined
with use of parallel composition and restriction
In this subsection we describe a process which is defined with use of the operations of parallel composition and restriction. This process is an implementation of a distributed algorithm of separation of sets. The problem of separation of sets has the following form. Let be a pair of finite disjoint sets, with each element is associated with a number , called a weight of this element. It is need to convert this pair to a pair of sets , such that
- •
(for each finite set the notation denotes a number of elements in )
- •
.
Below we shall call and as the left set and the right set, respectively.
The problem of separation of sets can be solved by an execution of several sessions of exchange elements between these sets. Each session consists of the following actions:
- •
find an element with a maximum weight in the left set
- •
find an element with minimum weight in the right set
- •
transfer
- –
from the left set to the right set, and
- –
from the right set to the left set.
To implement this idea it is proposed a distributed algorithm, defined as a process of the form
[TABLE]
where
- •
the process executes operations associated with the left set, and
- •
the process executes operations associated with the right set.
The restriction of the actions with names and in (29) means that a transmission of objects with names and can be executed only between the subprocesses and , i.e. such objects can not be transmitted outside the process (29).
A flow graph (i.e. a relation between components) corresponded to this process has the form
[TABLE]
Below we shall use the following notations: for each subset the records and denote an element of with maximum and minimum weight, respectively. A similar meaning have the records and , where is a a variable whose values are subsets of .
The process Small has the following form:
[TABLE]
(a double circle denotes an initial state).
An initial condition of the process is .
The process Large has the following form:
[TABLE]
An initial condition of the process is .
A process which is obtained by a simplification of the process (29) has the following form:
[TABLE]
This simplified process allows to detect some simple flaws of the algorithm of separation of sets, for examle a possibility of a deadlock situation: there are states of the process (32) (namely, and ) such that
- •
there is no transitions starting at these states
- •
but falling into these states is not a normal completion of the process.
13 Another example of
a simplification of a process
Suppose we have a system “multiplier”, which has
- •
two input ports with the names and , and
- •
one output port with the name .
An execution of the multiplier is that it
- •
receives on its input ports two values, and
- •
gives their product on the output port.
A behavior of the multiplier is described by the process :
[TABLE]
Using this multiplier, we want to build a system “calculator of a square”, whose behavior is described by the process :
[TABLE]
The desired system is a composition of
- •
the auxiliary system “duplicator” having
- –
an input port , and
- –
output ports and
behavior of which is described by the process :
[TABLE]
i.e. the duplicator copies its input to two outputs, and
- •
the multiplier, which receives on its input ports those values that duplicator gives.
A process , corresponding to such a composition is defined as follows:
[TABLE]
A flow graph of the process has the form
[TABLE]
However, the process does not meet the specification (i.e. and are not observationally equivalent). This fact is easy to detect by a construction of a graph representation of , which, by definition of operations of parallel composition, restriction and renaming, is the following:
[TABLE]
After a simplification of this process we obtain the process
[TABLE]
which shows that
- •
the process can execute two input actions together (i.e. without an execution of an output action between them), and
- •
the process can not do that.
The process meets another specification:
[TABLE]
where is a buffer which can store one message, whose behavior is represented by the diagram
[TABLE]
A flow graph of has the form
[TABLE]
A simplified process has the form
[TABLE]
The statement that meets the specification can be formalized as
[TABLE]
We justify (35) with use of theorem 7.2. At first, we rename variables of the process (34), i.e. instead of (34) we shall consider the process
[TABLE]
To prove with use of theorem 7.2 we define the formulas (where ) as follows:
- •
, if
- •
- •
- •
.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] R. Milner: A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer Verlag (1980)
- 2[2] R. Milner: Communicating and Mobile Systems: the π 𝜋 \pi -calculus. Cambridge University Press (1999)
- 3[3] C.A.R. Hoare: Communicating Sequential Processes. Prentice Hall (1985)
- 4[4] Clarke, E.M., Grumberg, O., and Peled, D.: Model Checking, MIT Press (1999)
- 5[5] C.A. Petri: Introduction to general net theory. In W. Brauer, editor, Proc. Advanced Course on General Net Theory, Processes and Systems, number 84 in LNCS, Springer Verlag (1980)
- 6[6] J.A. Bergstra, A. Ponse, and S.A. Smolka, editors: Handbook of Process Algebra. North-Holland, Amsterdam (2001)
- 7[7] D. Brand, P. Zafiropulo: On Communicating Finite-State Machines. Journal of the ACM, Volume 30 Issue 2, April 1983, pp. 323-342. ACM New York, NY, USA (1983)
- 8[8] R.W. Floyd: Assigning meanings to programs. In J.T. Schwartz, editor, Proceedings Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, pages 19-32. AMS (1967)