# Quantitative Analysis of Software Approximate Correctness

Authors: Yanfang Ma
Journal: Mathematical Problems in Engineering
 (2015)

---

## Abstract

Parameterized bisimulation provides an abstract description of software correctness. In real world situations, however, many software products are approximately correct. To characterize the approximate correctness, we generalize the parameterized bisimulation to numerical version and probabilistic setting. First, we propose the definition of the parameterized bisimulation index that expresses the degree to which a binary relation is parameterized bisimulation. Then,λ-parameterized bisimulation over environment e and its
substitutivity laws are presented. Finally, λ-parameterized probabilistic bisimulation is established to describe complicated software products with probabilistic phenomena.


---

## Body

## 1. Introduction

Correctness is a key feature of software trustworthiness [1–3], which can be abstracted by using various behavior equivalences between processes, such as (strong and weak) bisimilarity, trace equivalence, testing equivalence, and failure equivalence [4–6]. Specification and implementation of software are considered as two processes. If a certain behavior equivalence exists between specification and implementation, then the software is considered as correctness. Thus a certain behavior equivalence must be established between specification and implementation to prove software correctness.However, the prerequisites for successful application of software products may not always hold when they are actually running on the computers. As physical devices, computers cannot be assumed to behave reliably. In addition, standard implementations at best approximate the formal definition of semantics. Ying [7] proposed strong/weak bisimulation indexes to establish the approximate description between specification and implementation. The proposed indexes characterize the degree to which a binary relation between processes is strong/weak bisimulations. Ying and Wirsing [8] presented the strong/weak bisimulation limits and obtained the strong/weak bisimulation topologies to describe that the sequence of implementations can be treated as an evolution toward the specification. Girard and Pappas [9] defined a hierarchy of approximate pseudometric between two systems that quantifies the qualities of the approximations. To verify whether a program behaved as desired, Henzinger [10] introduced quantitative fitness measures for programs, particularly to measure the function, performance, and robustness of reactive programs such as concurrent processes. To compare these existing quantitative models of program approximate correctness, Fahrenberg and Legay [11] presented a distance-agnostic approach to quantify the verification. They defined a spectrum of different interesting system distances that corresponds to the given trace distance.In fact, some complicated software products contain probabilistic phenomena. These software products can be abstracted as probabilistic processes. Similarly, many quantitative models based on probabilistic processes [12] have existed to obtain the degree to which implementations satisfy their specification. For example, Giacalone et al. [13, 14] presented ε-bisimulation equivalence relation over deterministic probabilistic processes and proposed a kind of measure model to describe the degree of similarity among probabilistic processes. This measure is defined based on the probability differences of the processes that execute the same action. Song et al. [15] proposed a measure model according to the probability of the processes that performs the same trace with a discount factor. Deng et al. [16] defined state-metrics as a natural extension of bisimulation from nonquantitative systems to quantitative ones over action-labeled quantitative systems. Alves de Medeiros et al. [17] built a measure relation based on the observable actions of processes. Abate [18] also established an approximate metric based on probabilistic bisimulation.However, the running of a software depends on its environment. The environment should be considered when the approximation degree between specification and implementation is discussed. The influences of the environment are absent in the existing quantitative models. In [19], Larsen and Skou presented two-thirds bisimulation based on probabilistic transition systems to characterize that two processes are undistinguished when they have the same sets of observations for all tests. If an environment is considered as a set of actions [20], then two-thirds bisimulation expresses the relation in which the process refuses the environment. We proposed two-thirds simulation index and established a measure model to describe the degree of approximation among processes [21]. In π-calculus [22] and applied π-calculus [23], the observation equivalences were researched. And the influence of environment on the execution of software was considered as well. In [22], a process context is speaking a process expression containing a hole. In [23], the contexts may be used to represent the adversarial environment in which a process is run. The environment provides the data that the process inputs and consumes the data that it outputs.Larsen [24] presented parameterized bisimulation equivalence to obtain flexible hierarchic development methods. In the work of Larsen, bisimulation equivalence is parameterized with information about context called environment. Environment e is considered as an object that consumes the actions produced by a process in that environment. However, the abilities of environment to consume actions might be limited. Suppose that P is a process, and it can execute action α to next process P′; that is, P→αP′. However, e cannot consume the action α; then derivation P→αP′ will never be considered when P is executed in environment e. If P and Q both perform the same action for all transitions of e, then we can determine P~eQ. In particular, strong bisimulation in CCS (Communication and Concurrency Systems) model is generalized by parameterized bisimulation equivalence. Parameterized limit bisimulation and parameterized bisimulation limit were proposed in [25, 26] to describe the infinite evolution mechanism.The conditions possessing the same observable actions consumed by the environment are rigorous when we choose parameterized bisimulation to verify software correctness. Sometimes we can determine that two processes fail to meet these conditions. However, these processes are still close to parameterized bisimulation in the sense that whenever a process can execute an action of environment consumption, another process can produce an action that is different from but highly similar to the observable action that the first process executed. Alternatively, another process can perform an action that is highly similar to the observable action that the first process made whenever a process can produce an action that is different from the action of the environment consuming.The aim of this study is to build mathematical tools that are suitable for describing this kind of approximate parameterized bisimulation. First, we propose parameterized bisimulation index over environmente in order to describe the degree to which binary relation Re is a parameterized bisimulation. Then we define λ-parameterized bisimulation and discuss algebraic properties. We specially prove the congruence of λ-parameterized bisimulation under various operators. Finally, in order to describe the characterization of software with probabilistic information, we also extend parameterized bisimulation to probabilistic setting and propose the approximate parameterized probabilistic bisimulation.Compared with the main focuses of [7, 8, 21], the main focus of our work is on parameterized bisimulation. In [7, 8], the set of labels in a labeled transition system is equipped with a metric. Given a binary relation between processes, the degree to which the relation is bisimulation is defined. Similar to [7, 21], we also equip the set of actions with a metric. Parameterized bisimulation that includes the information about context is different from bisimulation. For every environment e, Re is a binary relation between processes. Therefore, in order to obtain the approximate parameterized bisimulation, we need to establish the bisimulation index for every environment e. We consider two cases to obtain the bisimulation index for an environment. One case is that when the environment consumes an action, a process can accept this action and another process cannot accept this action. Another case is that when the environment has the transition with an action, two processes cannot both accept this action. Therefore, our definition about bisimulation index on the environment is different from the definition of bisimulation index in [7]. Furthermore, we establish the λ-parameterized bisimulation on the environment e. In order to obtain the hierarchic development and modular decomposition of software, similar to [7, 21], we also consider the substitutivity laws of λ-parameterized bisimulation on the environment under various combinators.Meanwhile, we notice that many metric models are proposed based on the difference of probabilities in which two processes execute the same action [16]. But the influence of environment was not considered in these models. In order to describe the approximation of the complicated software with probabilistic information, we extend parameterized bisimulation to probabilistic setting in order to reflect the environment. First, we extend the environment transition system to probabilistic case. Then, we define parameterized probabilistic bisimulation. Finally, we obtain the λ-parameterized probabilistic bisimulation based on the probabilities that the environment consumes an action and the processes perform the same action. This point is similar to [14, 16]. Our method is different from the method in [18]. In [18], the state space is equipped with a rich structure, whereas the metric is characterized by probabilistic conditional kernels.In Section2, we recall the syntax of CCS and parameterized bisimulation. Parameterized bisimulation index over environment e and λ-parameterized bisimulation are defined in Section 3. Their some algebraic properties are researched in Section 3. In Section 4, the substitutivity laws of λ-parameterized bisimulation under various operators are proved. In Section 5, parameterized probabilistic bisimulation is proposed and λ-parameterized probabilistic bisimulation is defined. Furthermore, the congruence of λ-parameterized probabilistic bisimulation is proved. Our conclusions and future work are presented in Section 6.


## 2. Preliminaries

### 2.1. CCS Summary

This section recalls some fundamental concepts and the results of process calculus needed in the subsequent sections. The following definitions mainly come from the book by Ying [27].We introduce thenamesA, theconamesA¯, andlabelsΓ=A∪A¯. a,b,… range over A, a¯,b¯,… range over A¯, l,l′,… range over Γ is defined. We also introduce the silent or perfect action τ. Act=Γ∪{τ} is defined as the set ofactions, whereas α,β are defined range over Act. Furthermore, we introduce set ℵ of process variables and set K of processes constants. Mapping f:Γ→Γ is a relabeling function if f(l¯)=f(l)¯ for every l∈Γ. We may extend relabeling function f to be a mapping from Act to itself by decreeing that f(τ)=τ. The syntax of the basic process calculus is presented in the following definition.Definition 1 (process expression [28]).
The class∂ of process expressions is the smallest class of symbol strings that satisfies the following conditions:(1)
ℵ,K∈∂.(2)
Ifα∈Act and E∈∂, then α. E∈∂.(3)
IfI is an indexing set and Ei∈∂(i∈I), then ∑i∈IEi∈∂.(4)
IfE1,E2∈∂, then E1∣E2∈∂.(5)
IfE∈∂ and L⊆Γ, then E∖L∈∂.(6)
IfE∈∂ and f is a relabeling function, then E[f]∈∂.The process expressions without process variables are called processes and the class of processes is denoted byP. For any A∈R, we assume that there is a defining equation A=defPA, such as A=PA=l·A∈P. Constants provide us a mechanism of recursion in the process calculus.The transitional semantics of the basic calculus is presented in the style of Plotkin’s structural operational semantics [29]. We have the following definition.Definition 2 (labeled transition system [7]).
Let(∂,Act,{→α:α∈Act}) be a labeled transition system, where the transition relations →α(α∈Act) are presented by the following rules:(1)Actα.E→αE,SumjEj→αEj′∑i∈IEi→αEj′j∈I,Com1E→αE′E∣F→αE′∣F,Com2F→αF′E∣F→αF′∣F,Com3E→lE′F→l¯F′E∣F→τE′∣F′,ResE→αE′E∖L→αE′∖Lα,α¯∉L,RelE→αE′Ef→αE′f,ConP→αP′A→αP′A=defP.Transitions with strings of labels may be defined in a natural way. Ift=α1,…,αn∈Act∗=⋃n=0∞Actn, then we write E→tE′ provided that E→α1E1→α2⋯→αn-1En-1→αnE′ for some E1,…,En-1∈∂. In this case, we call t an action sequence of E and E′ is a t-derivative of E. If for some t∈Act∗,E′ is a t-derivative of E, then E′ is called a derivative of E.In the subsequent sections, we mainly consider the restriction(P,Act,{→αP:α∈Act}) of (∂,Act,{→α:α∈Act}) on P, where, for each α∈Act,→αP=→α∩(P×P) is restriction of →α on P. For simplicity, we always write →α for →αP.For example, suppose that a vending machine that sells CocaCola can be described as an expression of CCS:(2)P=1d.CocaCola.collect.P.Its behavior can be expressed as a transition diagram as in Figure1.Figure 1
An example of CCS.


### 2.2. Parameterized Bisimulation

The definition of environment must be introduced because the motivation of parameterized bisimulation is to parameterize the bisimulation equivalence with a special type of information about context called environment. Similar to the assumption that a process may change after performing an action, the assumption that an environment may change after consuming an action is reasonable. Thus environments and their behaviors can be described by labeled transition systemɛ=(Env,Act,⇒), where Env is the set of environments, Act is the set of actions (identical to the set of actions used in the transition system of process), and ⇒ is a subset of Env×Act×Env calledconsumption relation.  e⇒αe′ means that “e may consume the action α and in doing so become the environment e′.”At this point, let us review the parameterized bisimulation equivalence. First, we recall the bisimulation equivalence without environment.Definition 3 (bisimulation [24]).
BisimulationR is a binary relation on P such that whenever PRQ and α∈Act, then(1)
P→αP′⇒∃Q′ such that Q→αQ′ and P′RQ′,(2)
Q→αQ′⇒∃P′ such that P→αP′ and P′RQ′.Two processes,P and Q, are considered bisimulation if and only if bisimulation R exists and satisfies (P,Q)∈R.Definition 4 (ɛ-parameterized bisimulation [24]).
Letɛ=(Env,Act,⇒) be a transition system of environments. Then an ɛ-parameterized bisimulation, R, is an Env-indexed family of binary relations, Re⊆P×P for e∈Env, s.t. whenever PReQ and e⇒αf, then we have the following:(1)
IfP→αP′, then there exists Q′, s.t. Q→αQ′ and P′RfQ′.(2)
IfQ→αQ′, then there exists P′, s.t. P→αP′ and P′RfQ′.Two processes,P and Q, are said to be bisimulation equivalence in the environment e∈Env if and only if ɛ- parameterized bisimulation R exists, such that PReQ, which is denoted by P~eQ.Example 5 (see [24]).
Letɛ, P, and Q be presented by Figure 2. The Env-indexed family R is shown as follows:(3)Re0=P0,Q0.Re1=P1,Q1,P2,Q2,P1,Q5.Re2=P2,Q2,P1,Q1,P2,Q5.Re3=P3,Q6,P3,Q3.Re4=P4,Q7,P4,Q4.Figure 2
P
0 and Q0 are parameterized bisimulation on environment e0.We can prove thatR is a parameterized bisimulation. Thus, P0~e0Q0, P0≁Q0. Therefore, P0 can accept the action a, Q0 can also accept the same action, and their next states have the relation Re1 when the environment e0 can consume the action a to the next environment e1. By contrast, if Q0 can accept the action a, then P0 can also accept the same action, and their next states have the relation Re1. Similarly, P0 and Q0 have the same behavior when environment e0 can consume action a to the next environment e2. Thus, P0~e0Q0. However, according to Definition 3, we can observe that P0≁Q0.Although(P2,Q2)∈Re1,P2 and Q2 will never be considered when P2 and Q2 are executed in environment e1. The reason is that when e1 consumes the action b to the environment e3, P2 and Q2 cannot execute the action b to the next state.Proposition 6 (see [24]).
For alle∈Env and for all P,Q∈P, P~Q implies that P~eQ.This proposition indicates that parameterized bisimulation equivalence generalizes bisimulation equivalence.


## 2.1. CCS Summary

This section recalls some fundamental concepts and the results of process calculus needed in the subsequent sections. The following definitions mainly come from the book by Ying [27].We introduce thenamesA, theconamesA¯, andlabelsΓ=A∪A¯. a,b,… range over A, a¯,b¯,… range over A¯, l,l′,… range over Γ is defined. We also introduce the silent or perfect action τ. Act=Γ∪{τ} is defined as the set ofactions, whereas α,β are defined range over Act. Furthermore, we introduce set ℵ of process variables and set K of processes constants. Mapping f:Γ→Γ is a relabeling function if f(l¯)=f(l)¯ for every l∈Γ. We may extend relabeling function f to be a mapping from Act to itself by decreeing that f(τ)=τ. The syntax of the basic process calculus is presented in the following definition.Definition 1 (process expression [28]).
The class∂ of process expressions is the smallest class of symbol strings that satisfies the following conditions:(1)
ℵ,K∈∂.(2)
Ifα∈Act and E∈∂, then α. E∈∂.(3)
IfI is an indexing set and Ei∈∂(i∈I), then ∑i∈IEi∈∂.(4)
IfE1,E2∈∂, then E1∣E2∈∂.(5)
IfE∈∂ and L⊆Γ, then E∖L∈∂.(6)
IfE∈∂ and f is a relabeling function, then E[f]∈∂.The process expressions without process variables are called processes and the class of processes is denoted byP. For any A∈R, we assume that there is a defining equation A=defPA, such as A=PA=l·A∈P. Constants provide us a mechanism of recursion in the process calculus.The transitional semantics of the basic calculus is presented in the style of Plotkin’s structural operational semantics [29]. We have the following definition.Definition 2 (labeled transition system [7]).
Let(∂,Act,{→α:α∈Act}) be a labeled transition system, where the transition relations →α(α∈Act) are presented by the following rules:(1)Actα.E→αE,SumjEj→αEj′∑i∈IEi→αEj′j∈I,Com1E→αE′E∣F→αE′∣F,Com2F→αF′E∣F→αF′∣F,Com3E→lE′F→l¯F′E∣F→τE′∣F′,ResE→αE′E∖L→αE′∖Lα,α¯∉L,RelE→αE′Ef→αE′f,ConP→αP′A→αP′A=defP.Transitions with strings of labels may be defined in a natural way. Ift=α1,…,αn∈Act∗=⋃n=0∞Actn, then we write E→tE′ provided that E→α1E1→α2⋯→αn-1En-1→αnE′ for some E1,…,En-1∈∂. In this case, we call t an action sequence of E and E′ is a t-derivative of E. If for some t∈Act∗,E′ is a t-derivative of E, then E′ is called a derivative of E.In the subsequent sections, we mainly consider the restriction(P,Act,{→αP:α∈Act}) of (∂,Act,{→α:α∈Act}) on P, where, for each α∈Act,→αP=→α∩(P×P) is restriction of →α on P. For simplicity, we always write →α for →αP.For example, suppose that a vending machine that sells CocaCola can be described as an expression of CCS:(2)P=1d.CocaCola.collect.P.Its behavior can be expressed as a transition diagram as in Figure1.Figure 1
An example of CCS.


## 2.2. Parameterized Bisimulation

The definition of environment must be introduced because the motivation of parameterized bisimulation is to parameterize the bisimulation equivalence with a special type of information about context called environment. Similar to the assumption that a process may change after performing an action, the assumption that an environment may change after consuming an action is reasonable. Thus environments and their behaviors can be described by labeled transition systemɛ=(Env,Act,⇒), where Env is the set of environments, Act is the set of actions (identical to the set of actions used in the transition system of process), and ⇒ is a subset of Env×Act×Env calledconsumption relation.  e⇒αe′ means that “e may consume the action α and in doing so become the environment e′.”At this point, let us review the parameterized bisimulation equivalence. First, we recall the bisimulation equivalence without environment.Definition 3 (bisimulation [24]).
BisimulationR is a binary relation on P such that whenever PRQ and α∈Act, then(1)
P→αP′⇒∃Q′ such that Q→αQ′ and P′RQ′,(2)
Q→αQ′⇒∃P′ such that P→αP′ and P′RQ′.Two processes,P and Q, are considered bisimulation if and only if bisimulation R exists and satisfies (P,Q)∈R.Definition 4 (ɛ-parameterized bisimulation [24]).
Letɛ=(Env,Act,⇒) be a transition system of environments. Then an ɛ-parameterized bisimulation, R, is an Env-indexed family of binary relations, Re⊆P×P for e∈Env, s.t. whenever PReQ and e⇒αf, then we have the following:(1)
IfP→αP′, then there exists Q′, s.t. Q→αQ′ and P′RfQ′.(2)
IfQ→αQ′, then there exists P′, s.t. P→αP′ and P′RfQ′.Two processes,P and Q, are said to be bisimulation equivalence in the environment e∈Env if and only if ɛ- parameterized bisimulation R exists, such that PReQ, which is denoted by P~eQ.Example 5 (see [24]).
Letɛ, P, and Q be presented by Figure 2. The Env-indexed family R is shown as follows:(3)Re0=P0,Q0.Re1=P1,Q1,P2,Q2,P1,Q5.Re2=P2,Q2,P1,Q1,P2,Q5.Re3=P3,Q6,P3,Q3.Re4=P4,Q7,P4,Q4.Figure 2
P
0 and Q0 are parameterized bisimulation on environment e0.We can prove thatR is a parameterized bisimulation. Thus, P0~e0Q0, P0≁Q0. Therefore, P0 can accept the action a, Q0 can also accept the same action, and their next states have the relation Re1 when the environment e0 can consume the action a to the next environment e1. By contrast, if Q0 can accept the action a, then P0 can also accept the same action, and their next states have the relation Re1. Similarly, P0 and Q0 have the same behavior when environment e0 can consume action a to the next environment e2. Thus, P0~e0Q0. However, according to Definition 3, we can observe that P0≁Q0.Although(P2,Q2)∈Re1,P2 and Q2 will never be considered when P2 and Q2 are executed in environment e1. The reason is that when e1 consumes the action b to the environment e3, P2 and Q2 cannot execute the action b to the next state.Proposition 6 (see [24]).
For alle∈Env and for all P,Q∈P, P~Q implies that P~eQ.This proposition indicates that parameterized bisimulation equivalence generalizes bisimulation equivalence.


## 3. Approximate Parameterized Bisimulation

For the approximate version of parameterized bisimulation, we present the definition of parameterized bisimulation index over the environment that indicates the degree to which a binary relation is parameterized bisimulation. We also generalize some algebraic properties of parameterized bisimulation.Definition 7 (metric space [30]).
LetM be a nonempty set. ρ is a mapping from M×M into [0,∞]. Then the pair (M,ρ) is called a metric space if the following conditions are satisfied:(1)
ρ(x,y)=0 if and only if x=y.(2)
ρ(x,y)=ρ(y,x).(3)
ρ(x,z)≤ρ(x,y)+ρ(y,z) for any x,y,z∈M.If  (1) is weakened by 1′: ρ(x,x)=0 for each x∈M, then ρ is called a pseudometric. If (3) is strengthened by 3′: ρ(x,z)≤max⁡{ρ(x,y),ρ(y,z)} for any x,y,z∈M, then ρ is called an ultrametric.Letρ be a metric on A. As expected, we can extend ρ to a mapping from Act×Act to [0,∞], which is denoted by ρact in the following way: for any a,b∈A,(1)
ρact(τ,τ)=0,(2)
ρact(a,b)=ρact(a¯,b¯)=ρ(a,b),(3)
ρact(τ,b)=ρact(a,τ)=ρact(τ,b¯)=ρact(a¯,τ)=ρact(a,b¯)=ρact(a¯,b)=∞.ρ
a
c
t is clearly a metric on Act. In addition, ρact is also an ultrametric provided that ρ is an ultrametric. For simplicity, we always write ρ for ρact. Then the numerical generalization of Definition 4 will be defined. Similar to the parameterized bisimulation, the following assumption is obtained: if e1 can consume an action to e2, P and Q have the relation Re1, but no transitions exist that can make P and Q execute certain actions to obtain some states that are included in Re2, then P and Q will never be considered when P and Q are executed in e1.Definition 8.
Let(P,Act,{→αP:α∈Act}) be a labeled transition system and let ρ be a metric on Act.ɛ=(Env,Act,⇒) is an environment transition system. R is an Env-indexed family of binary relations Re⊆P×P. For e∈Env, e⇒αe′, and (P,Q)∈Re, we define that (4)bRe,e′;αP,Q=max⁡bRe,e′;α≠P,Q,bRe,e′;α=P,Q,where (5)
b
R
e
,
e
′
;
α
≠
P
,
Q
=
sup
⁡
b
R
e
,
e
′
;
α
≠
P
,
Q
′
;
t
:
Q
′
∈
P
and
t
∈
A
c
t
with
Q
⟶
t
Q
′
,
if
t
≠
α
,
b
R
e
,
e
′
;
α
=
P
,
Q
=
sup
⁡
b
R
e
,
e
′
;
α
=
P
,
Q
′
;
t
:
Q
′
∈
P
and
t
∈
A
c
t
with
Q
⟶
t
Q
′
if
t
=
α
,
b
R
e
,
e
′
;
α
≠
P
,
Q
′
;
t
=
inf
⁡
ρ
t
,
u
:
u
∈
A
c
t
and there is
P
′
∈
P
such that
P
⟶
u
P
′
and
ρ
u
,
α
-
ρ
t
,
α
≤
0
,
and
Q
′
R
e
′
P
′
,
if
t
≠
α
,
b
R
e
,
e
′
;
α
=
P
,
Q
′
;
t
=
inf
⁡
ρ
t
,
u
:
u
∈
A
c
t
and there is
P
′
∈
P
such that
P
⟶
u
P
′
,
and
Q
′
R
e
′
P
′
,
if
t
=
α
.
We callbR(e,e′;α)(P,Q) an index in which P simulates Q on the transition e⇒αe′.Definition 9.
Let(P,Act,{→αP:α∈Act}) be a labeled transition system and let ρ be a metric on Act. ɛ=(Env,Act,⇒) is an environment transition system. R is an Env-indexed family of binary relations Re⊆P×P. If e∈Env, such that (6)bRe=supbRe,e′;α:e⟹αe′,where (7)bRe,e′;α=sup⁡maxbRe,e′;αP,Q,bRe,e′;α-1Q,P:PReQ,then bRe is called parameterized bisimulation index of R over environment e.As expected, ifQ,Q′,P∈P, t∈Act and e⇒αe′ given, and PReQ and Q→tQ′, then bRe,e′;α=(P,Q′;t) and bRe,e′;α≠(P,Q′;t) are the infimum of distances between transitions t and u where t and u are close to α. From this point, Definition 9 is clearly a numerical counterpart of Definition 4 and bRe expresses the degree to which Re is parameterized bisimulation. We should indicate that the smaller the value of bRe, the higher the degree to which Re is a bisimulation. We can obtain the conclusion that, for every e∈Env, bRe=0 when R is parameterized bisimulation.Proposition 10.
(1)R is parameterized bisimulation if and only if, for every e∈Env, bRe=0. In particular, bIdRe=0, where IdRe is the identical relation between processes.
(2) For alle∈Env, bRe-1=bRe.
(3) For alle∈Env, bRe1∘Re2≤bRe1+bRe2. In particular, if ρ is an ultrametric, then bRe1∘Re2≤max{bRe1,bRe2}.
(4) For alle∈Env, b⋃i∈IRei≤supi∈I⁡bRei.Proof.
(
1
) and (2) are direct from Definition 9.
(
3
) If bRe1=∞ or bRe2=∞, then it is clear. At this point, suppose that bRe1<∞ and bRe2<∞. Sequences {λ1n} and {λ2n} exist, such that bRe1<λ1n and bRe2<λ2n(n=1,2,…), limn→∞⁡λ1n=bRe1, limn→∞⁡λ2n=bRe2, for any e⇒αe′, bR(e,e′;α)1≤λ1n, and bR(e,e′;α)2≤λ2n.
For anyP,W∈P, if P(Re1∘Re2)W, then there exists Q∈P with PRe1Q and QRe2W. For any P′∈P and t1∈Act, P→t1P′. If t1=α, then bR(e,e′;α)1=<λ1n leads to the idea that there exist Q′∈P and t2∈Act such that Q→t2Q′, P′Re′1Q′, and ρ(t1,t2)≤λ1n. At the same time, if t1≠α, bR(e,e′;α)1≠<λ1n also leads to the idea that there exist Q′∈P and t2∈Act such that Q→t2Q′ with ρ(t2,α)≤ρ(t1,α), P′Re′1Q′, and ρ(t1,t2)≤λ1n.
Furthermore,bR(e,e′;α)2<λ2n leads to the following: if t1=α, bRe,e′;α2=(W,Q′;t2)≤λ2n. Thus, W′∈P and t3∈Act exist, such that W→t3W′ with ρ(t2,t3)<λ2n and Q′Re′2W′. Moreover, if t1≠α, bRe,e′;α2≠(W,Q′;t2)≤λ2n. We can obtain W′∈P and t3∈Act such that W→t3W′ with ρ(t3,α)≤ρ(t2,α), Q′Re′2W′, and ρ(t2,t3)<λ2n. Therefore, P′Re′1∘Re′2W′ with ρ(t3,α)≤ρ(t1,α) and ρ(t1,t3)≤ρ(t1,t2)+ρ(t2,t3)<λ1n+λ2n.bRe1∘Re2≤λ1n+λ2n(n=1,2,…). And bRe1∘Re2≤limn→∞⁡λ1n+λ2n=limn→∞⁡λ1n+limn→∞⁡λ2n=bRe1+bRe2.
(
4
) is similar to (3).(1) in Proposition10 indicates that, for any e∈Env, the parameterized bisimulation index is 0, which is the least value of the bisimulation index over the environment e. (2) states that, for any environment e∈Env, the bisimulation index of relation Re and the bisimulation index of its inverse are the same. (3) means that, for any environment e∈Env, the bisimulation index of the composition of two relations is not greater than the sum of the bisimulation indexes of the relation. If the presumed metric on actions is an ultrametric, then it does not exceed even the greatest of the bisimulation indexes of the factor relations. Finally, (4) means that if the degree to which Rei is a bisimulation is not less than some values for all i∈I, then the degree to which ⋃i∈IRei is a bisimulation is also not less than that value.Example 11.
Letɛ and P, Q be illustrated by Figure 3. The Env-indexed family R is shown as follows:(8)Re0=P0,Q0,Re1=P1,Q1,P2,Q2,P1,Q5,Re2=P2,Q2,P1,Q1,P2,Q5,Re3=P3,Q6,P3,Q3,Re4=P4,Q7,P4,Q4.Figure 3
An example of parameterized bisimulation index.Let the metric onAct be defined as (9)ρa,b=ρb,a=0.1,ρa,c=ρc,a=0.6,ρa,d=ρd,a=0.6,ρb,c=ρc,b=0.7,ρb,d=ρd,b=0.4,ρc,d=ρd,c=0.8.Then, we can obtain thatbRe0=0.1, bRe1=0.1, bRe2=0, and bRe3=bRe4=0.In fact, given thate0⇒ae1, we should first compute bR(e0,e1;a) when bRe0 is computed. Moreover, (P0,Q0)∈Re0 leads to the idea that bR(e0,e1;a)(P0,Q0) and bR(e0,e1;a)-1(Q0,P0) should be gained. Since Q0→aQ1, we only need to compute bR(e0,e1;a)=(P,Q1;t=a). By P0→bP1 and (P1,Q1)∈Re1, the metric ρ(b,a)=0.1 can be obtained according to Definition 9. Meanwhile, P0→bP2, but (P2,Q1)∉Re1, so this transition should not be considered. Thus, we obtain bR(e0,e1;a)=(P,Q1;t=a)=0.1. Similarly, we get that bR(e0,e1;a)=(P,Q2;t=a)=0.1, bR(e0,e1;a)=(P,Q3;t=a)=0.1. Thus bR(e0,e1;a)=(P0,Q0)=0.1.By contrast, we only need to computebR(e0,e1;a)-1≠(Q0,P0) when P0→bP1 because b≠a. Furthermore, we should obtain bR(e0,e1;a)-1≠(Q0,P1;b). Since ρ(a,b)=0.1, we only choose the transition of Q0 which satisfies the metric between a and the action u of Q0 executing less than ρ(b,a). All transitions of Q0 both satisfy the metric between a and the actions that Q0 can perform is less than and equal to 0.1. However, (P1,Q2)∉Re1. Thus, we can obtain bR(e0,e1;a)-1≠(Q0,P1;b)=0.1. Similarly, we can gain bR(e0,e1;a)-1≠(Q0,P2;b)=0.1. Thus, bR(e0,e1;a)-1≠(Q0,P0)=0.1. Moreover, bR(e0,e1;a)=0.1. Furthermore, we also get bR(e0,e2;a)=0.1 when e0⇒ae2. Therefore, bRe0=0.1.In particular,(P2,Q2) will never be considered when we compute bRe1 and e1⇒be3. The reason is that the next states of (P2,Q2) are not in Re3. The other results can be obtained in the same way.Proposition 12.
Letɛ=(Env,Act,⇒) be an environment transition system. If R is a strong bisimulation relation, then, for every e∈Env, bR=bRe, where bR is the bisimulation index defined in [7].Definition 13.
Letσ=(P,Act,{→α:α∈Act}) be a labeled transition system. ɛ=(Env,Act,⇒) is an environment transition system. R is an Env-indexed family of binary relations on P×P; that is, Re⊆P×P for e∈Env, λ∈[0,∞). If bRe≤λ, then Re is called a λ-parameterized bisimulation over the environment e.IfR is an Env-indexed family of binary relations on P×P, e∈Env, then Re is clearly an ∞-parameterized bisimulation. If λ1≤λ2 and Re is λ1-parameterized bisimulation, then Re is also a λ2-parameterized bisimulation. Moreover, if Re is λi-parameterized bisimulation (i∈I), then Re is a infi∈I⁡λi-parameterized bisimulation.Corollary 14.
Letσ=(P,Act,{→α:α∈Act}) be a labeled transition system. ɛ=(Env,Act,⇒) is an environment transition system. R is an Env-indexed family of binary relations on P×P.(1)
IfR is a parameterized bisimulation, then, for any environment e∈Env, Re is a 0-parameterized bisimulation.(2)
IfR is a parameterized bisimulation, e∈Env, Re is a λ-parameterized bisimulation, if and only if so is Re-1.(3)
If, fore∈Env, Rei is a λi-parameterized bisimulation (i=1,2), then Re1∘Re2 is a λ1+λ2-parameterized bisimulation. In particular, if ρ is an ultrametric and R1 and R2 are all λ-bisimulation, so is R1∘R2.(4)
If, fore∈Env, Rei is a λ-bisimulation (i∈I), so is ⋃i∈IRei.Using the concept ofλ-bisimulation, we can define the notion of λ-parameterized bisimulation in the usual way over the environment e.Definition 15.
LetR be an Env-indexed family of binary relations on P×P. For any λ∈[0,∞), we define λ-bisimulation over the environment e as (10)
~
e
λ
=
⋃
R
e
∣
R
e
is
a
λ
-parameterized bisimulation over the environment
e
.In other words, if(P,Q)∈Re, then P and Q are said to be λ-bisimilar over the environment e whenever λ-parameterized bisimulation R exists such that (P,Q)∈Re. If (P,Q)∈Re, e can consume some actions to e′, but P and Q do not have any transition such that their next states are included in Re′, then P and Q will never be considered when P and Q are executed in the environment e.Next, we illustrate Definitions9 and 15 with the following example.Example 16.
Two vending machines are assumed to exist. They can be expressed by the following process expressions:(11)P=1d.CocaCola.Collect.PQ=1.2d.CocaCola.Collect+0.7.Fanta.Collect.Q.A person who wants to buy a cup of CocaCola can be treated as an environment of the vending machines. According to CCS, the behaviors of the person can be described as a process: (12)ɛ=1d.CocaCola.Collect.ɛ.The transition diagrams are described in Figure 4. Metric ρ exists on the set of actions Act, where Act={1d,1.2d,0.7d,CocaCola,Fanta,Collect}. Consider ρ(1d,1.2d)=0.2, ρ(1d,0.7)=0.3, ρ(1.2d,0.7d)=0.5, and ρ(CocaCoca,Fanta)=0.2. The distance between other actions is ∞.Figure 4
P
0 and Q0 are 0.3-bisimilar on the environment e0.The following relations can be defined:(13)Re0=P0,Q0Re1=P1,Q1,P1,Q2Re2=P2,Q3,P2,Q4.We can get thatbRe0=0.3, bRe1=0.2, bRe2=0. So, P0~e00.3Q0, P1~e10.2Q1, P1~e10.2Q2, P2~e20Q3, and P2~e20Q4. The value means that when the person does not do anything, the approximate degree between two vending machines is 0.7. When the person puts 1d, then the approximate degree between two vending machines is 0.8. Finally, when the person chooses the CocaCola, the distance between them is 0.Next, we will try to prove various properties ofλ-parameterized bisimulation over environment e.Proposition 17.
Consider
(1)~e⊆~e0. If λ1≤λ2, then ~eλ1⊆~eλ2.
(2) For anyλ∈[0,∞), ~eλ is a λ-parameterized bisimulation and it is reflexive and symmetric; ~eλ1∘~eλ2=~eλ1+λ2.Proposition 18.
Lete∈Env. s1~eλs2 if and only if, for any e⇒αe′, b(~eλ)(e,e′;α)(s1,s2)≤λ and b(~eλ)(e,e′;α)(s2,s1)≤λ.Proof.
Ifs1~eλs2, then we have that b(~eλ)(e,e′;α)(s1,s2)≤λ and b(~eλ)(e,e′;α)(s2,s1)≤λ.
Conversely, we define that(s1,s2)∈Re if and only if b(~eλ)(e,e′;α)(s1,s2)≤λ and b(~eλ)(e,e′;α)(s2,s1)≤λ for all e⇒αe′. From b(~eλ)(e,e′;α)(s1,s2)≤λ, we know that, for any s1′∈P and t∈Act with s1→ts1′, if t=α, then, for any n≥1, there exist s2′∈P and t∈Act such that s2→t′s2′ and ρ(t,t′)<λ+1/n and s1′~e′λs2′; if t≠α, then, for any n≥1, there exist s2′∈P and t∈Act such that s2→t′s2′ and ρ(t′,α)≤ρ(t,α), ρ(t,t′)<λ+1/n, and s1′~e′λs2′. By noting that s1′~e′λs2′ implies s1′Re′s2′, we obtain bR(e,e′;α)(s1,s2)≤λ. Similarly, bR(e,e′;α)-1(s2,s1)≤λ. Therefore, Re is a λ-parameterized bisimulation over the environment e, and s1~eλs2.


## 4. Congruence ofλ-Parameterized Bisimulation over Environment e

In order to support hierarchic development and modular decomposition of software, it is necessary to ensure that equivalences are congruent with respect to processes combinators. It means that if two processes are equivalent, then the new processes obtained by combining the given processes are also equivalent. In this section, we will mainly discuss these substitutivity laws ofλ-parameterized bisimulation under various combinators.Definition 19 (λ-round [7]).
Let(M,ρ) be a metric space; Y⊆M,λ≥0. If, for any x,y∈M,x∈Y and ρ(x,y)≤λ implies y∈Y, then Y is said to be λ-round. If, for some μ>λ,Y is μ-round, then Y is said to be strongly λ-round.Definition 20 (isomorphism mapping [7]).
Let(M,ρ) be a metric space. f is a mapping from M into itself. If, for any x,y∈M,ρ(f(x),f(y))=ρ(x,y), then f is said to be isomorphism mapping.From the definition above, we can see thatλ-round is a rigorous condition. In [7], they prove that there are only two λ-round sets in the real line when λ>0. One is the empty set and the other is the real line itself. They also show that it is not the same case as in the real line in general. For example, if M=⋃i∈IMi and {Mi}i∈I is pairwise disjoint and ρ(x,y)>μ for any x,y∈M with x∈Mi and y∈Mj(i≠j), then each Mi is λ-round for every λ≤μ.We now consider the substitutivity laws ofλ-parameterized bisimulation over environment e under various combinators in our process calculus.Proposition 21.
Letɛ=(Env,Act,⇒) be an environment transition system; e∈Env,(1)
IfP1~eλP2 and e′⇒αe, then α·P1~e′λα·P2.(2)
IfL is λ-round and P1~eλP2, then P1∖L~eλP2∖L.(3)
Iff is isomorphism mapping on Act and P1~f-1(e)λP2, then P1[f]~eλP2[f].(4)
IfP1~eλP2, then W+P1~eλW+P2.Proof.
(
1
) We need to show b(~e′λ)(e′,e;α)(α·P1,α·P2)≤λ and b(~e′λ)(e′,e;α)(α·P2,α·P1)≤λ. By Definition 2, α·P1→αP1 and P1~eλP2, so there exists P2 such that α·P2→αP2 with ρ(α,α)≤ρ(α,α) and ρ(α,α)=0≤λ. So b(~e′λ)(e′,e;α)(α·P1,α·P2)=0≤λ. Similarly, b(~e′λ)(e′,e;α)(α·P2,α·P1)=0≤λ.
(
2
) Let e∈Env, Se={(P1∖L,P2∖L):P1~eλP2}. Next, we need to show bSe≤λ.
Lete⇒βf. If P1∖L→αP1′, then α,α′∉L∪L¯, P1⇒αP1′′, and P1′=P1′′∖L. If α≠β, since P1~eλP2, there exist P2′′∈P and u∈Act such that P2→uP2′′ with ρ(u,β)≤ρ(α,β), ρ(α,u)≤λ, and P1′′~fλP2′′. Since L is λ-round, u,u¯≠L∪L¯. By the transition rule, P2∖L→uP2′′∖L=P2′ with ρ(u,β)≤ρ(α,β), ρ(α,u)≤λ, and (P1′,P2′)∈Sf. If α=β, then P1~eλP2 leads to the idea that there exist P2′′∈P and u∈Act such that P2→uP2′′ with ρ(α,u)≤λ and P1~fλP2′′. Since L is λ-round, u,u¯≠L∪L¯. By the transition rule, P2∖L→uP2′′∖L=P2′ with ρ(α,u)≤λ and (P1′,P2′)∈Sf. Therefore, bSe≤λ.
(
3
) For any e∈Env, let Se={(P1[f],P2[f]):P1~f-1(e)λP2}. Next, we only need to show bSe≤λ.
In fact, lete⇒bg. If P1f→αP1′, then there exists h∈Act, such that P1→hP1′′, P1′′[f]=P1′, and α=f(h). If α≠b, since P1~f-1(e)λP2, f-1(e)⇒f-1(b)f-1(g) and there exist P2′′∈P and u∈Act such that P2→uP2′′ with ρ(h,u)≤λ, ρ(u,f-1(b))≤ρ(h,f-1(b)), (P1′′,P2′′)∈Sf-1(g), and P1′′~f-1gλP2′′. By the transition rule, P2f→fuP2′′[f]. Let P2′=P2′′[f] and since f is isomorphism, ρ(f(u),b)=ρ(f(u),f(f-1(b)))=ρ(u,f-1(b))≤ρ(h,f-1(b))=ρ(f(h),b) and ρ(f(u),f(h))=ρ(u,h)≤λ, and (P1′′[f],P2′′[f])∈Sg.
On the other hand, ifα=b, P1~f-1(e)λP2 tells us f-1(e)⇒f-1(b)f-1(g) and there exist P2′′∈P and u∈Act such that P2→uP2′′ with ρ(h,u)≤λ, (P1′′,P2′′)∈Sf-1(g), and P1′′~f-1(g)λP2′′. By the transition rule, P2f→fuP2′′[f]. Let P2′=P2′′[f] and since f is isomorphism, ρ(f(u),f(h))=ρ(u,h)≤λ, and (P1′′[f],P2′′[f])∈Sg. Therefore, bSe≤λ.
(
4
) We need to prove that, for any e⇒be′, b(~eλ)(e,e′;b)(W+P1,W+P2)≤λ and b(~eλ)(e,e′;b)(W+P2,W+P1)≤λ. In fact, if W+P1→αP′, then P1→αP1′ or W→αP1′. Furthermore, if α≠b, then P1→αP1′ leads to the idea that there exist P2′∈P and β∈Act such that P2→βP2′ with ρ(β,b)≤ρ(α,b), ρ(α,β)≤λ, and (P1′,P2′)∈~fλ. So, W+P2→βP2′, and b(~eλ)(e,e′;b)(W+P1,W+P2)≤λ. And if W→αP1′, then W+P2→αP1′, and (P1′,P1′)∈~e0, so (P1′,P1′)∈~eλ. Thus, b(~eλ)(e,e′;b)(W+P1,W+P2)≤λ.
On the other hand, ifα=b, then P1→αP1′ leads to the idea that there exist P2′∈P and β∈Act such that P2→βP2′, with ρ(α,β)≤λ and (P1′,P2′)∈~fλ. So, W+P2→βP2′, and b(~eλ)(e,e′;b)(W+P1,W+P2)≤λ. And W→αP1′ tells us W+P2→αP1′, (P1′,P1′)∈~e0, and (P1′,P1′)∈~eλ. Thus, b(~eλ)(e,e′;b)(W+P1,W+P2)≤λ.
Similarly, we can obtain thatb(~eλ)(e,e′;b)(W+P2,W+P1)≤λ. So, W+P1~eλW+P2.


## 5. Parameterized Probabilistic Bisimulation

The behaviors of some complicated software systems are often probabilistic in nature. Usually, a system with probabilistic behaviors may typically be described as a probabilistic process. van Glabbeek et al. [31] introduced three models of probabilistic processes in accordance with the relation between the occurrences of actions and transition probabilities: a reactive system, a generative system, and a stratified model. For example, Larsen and Skou [19] adopted a reactive model for probabilistic processes; Giacalone et al. [14] considered generative probabilistic processes. The probabilistic processes dealt by Smolka and Steffen [32] are in a stratified setting. These models are the extension of SCCS proposed by Milner [33]. Ying [34] proposed a new model of probabilistic process, APPA, which is a probabilistic extension of CCS. Giacalone et al. [13] relaxed the notion of probabilistic bisimulation on the class of deterministic PCCS processes, called ϵ-bisimulation. Two processes can simulate each other with bound ϵ of deviation in probability. Furthermore, a natural notion of distance between deterministic PCCS processes and an accompanying metric space are proposed.However, to show the effect of environment on the execution of software, we can extend parameterized bisimulation to the probabilistic case. Firstly, the syntax and semantics of the probabilistic processes are reviewed. As in SCCS [33], let (Act,×,1) be the Abelian monoid. Intuitively, action of the form α×β represents the simultaneous execution by a process of the actions α and β. It will often use juxtaposition to denote products of actions, for example, αβ. It is convenient to assume that ∀α∈A,∃α¯∈A¯:α×α¯=α¯×α=1 and vice versa.Then(Act,×,1,-) is an Abelian group. Let A be a subset of Act such that 1∈A and let f:Act→Act be a monoid morphism. X is assumed as a process variable. The syntax of PCCS is defined as the following definition.Definition 22 (the syntax of PCCS [13]).
The set of probabilistic process expressions is the smallest set which includes0, X, and the following expressions: (14)E⩴α·E∣∑i∈IpiEi,pi∈0,1,∑i∈Ipi≤1E×F∣E↾A∣EffixXE.An expression that has no free variables is called a process, andPr is the set of all PCCS processes. Intuitively, 0 has no derivations, whereas α·E performs action α with probability 1 and then behaves like E. A summation expression offers a probabilistic choice among its constituent behaviors, where I is accountable, so ∑i∈Ipi is a probabilistic distribution. When I=∅, then 0=∑i∈∅Ei. Product represents synchronized process composition. For the restricted expression E↾A, only actions in A are visible to an observer, while morphism specifies relabeling of actions. Finally fixXE defines a recursive process.Then, similar to [13], we introduce an unindexed arrow that represents the cumulative probabilistic derivation of one process by another. For P,Q∈Pr and α∈Act, we write P→α[p]Q exactly when p=∑{pi∣P→iα[pi]Q}, where the indices i that appear on the arrows are used to distinguish different occurrences of the same probabilistic derivation. For P∈Pr, S⊆Pr, and α∈Act, we write P→α[p]S exactly when p=∑Q∈S{q∣P→α[q]Q}.LetDPr be the class of deterministic PCCS processes; that is, if P∈DPr, then, for any α∈Act, P has at most one probabilistic derivation of type α. Then, the operational semantics of deterministic PCCS process can be described as follows.Definition 23 (see [13]).
The structure operational semantics of deterministic PCCS process based on probabilistic derivation is given as a set of inference rules, in the style of Plotkin:(15)Actα·E→α1E,SumjEj→αqE′⟹∑i∈IpiEi→αpj·qE′j∈I,ProE→αpE′,F→βqF′⟹E×F→αβp·qE′×F′,ResE→αpE′⟹E↾A→αp/υE,AE′↾Aα∈A,whereυE,A=∑pi∣E→αpiE′,α∈A,RelE→αpE′⟹Ef→fαpE′f,ConEfixXEX→αpE′⟹fixXE→αpE′.Similar to the assumption on parameterized bisimulation, the assumption that an environment and its behaviors can be described as a deterministic PCCS process is reasonable.Env is the set of environments, Act is the set of actions (identical to the set of actions used in the transition system of processes), and ⇒ is a subset of Env×Act×[0,1]×Env, and e⇒α[p]e′ means that e may consume the action α with the probability p and after that becomes the environment e′.Then, parameterized probabilistic bisimulation is defined.Definition 24.
Letɛ=(Env,Act,⇒) be a probabilistic environment transition system. Then an ɛ-parameterized probabilistic bisimulation, R, is an Env-indexed family of binary relations Re⊆DPr×DPr for e∈Env, such that whenever (P,Q)∈Re and e⇒α[p]f, then we have the following: (i)
IfP→α[p]P′, then there exists Q′∈DPr s.t. Q→α[p]Q′ and P′,Q′∈Rf.(ii)
IfQ→α[p]Q′, then there exists P′∈DPr s.t. P→α[p]P′ and P′,Q′∈Rf.Define(16)~epr=Re∣Reis parameterized probabilistic bisimulation over the environmente.Two processes, P and Q, are said to be probabilistic bisimulation equivalence on the environment e∈Env if and only if there exists ɛ-parameterized probabilistic bisimulation R such that (P,Q)∈Re. We write parameterized probabilistic bisimulation by using the following signal, P~eprQ, to distinguish the difference between parameterized bisimulation and parameterized probabilistic bisimulation.Example 25.
Letɛ, P, and Q be given in Figure 5. The Env-indexed family R is shown as follows: (17)Re0=P0,Q0Re1=P1,Q1,P2,Q2,P1,Q2Re2=P2,Q2Re3=P3,Q3,P3,Q5Re4=P4,Q4,P4,Q6.Figure 5
P
0 and Q0 are probabilistic bisimulation on the environment e0.Then, according to Definition24, R is ɛ-parameterized probabilistic bisimulation. So, P0~e0prQ0, P1~e1prQ1, P1~e1prQ2, but P2≁e1prQ2, P2≁e2prQ2.Next, we try to relax theɛ-parameterized probabilistic bisimulation to establish the approximate parameterized probabilistic bisimulation. In [18], there is a rather rich state-space structure and a metric between two processes employs the probabilistic conditional kernels underlying the two stochastic processes. Another metric is based on the dynamical properties of the two processes. Compared with the metric in [18], our model only focuses on the difference of probabilities where two processes can execute the same action.Definition 26.
Letɛ=(Env,Act,⇒) be a probabilistic environment transition system. Consider λ∈[0,1]. R is an Env-indexed family of binary relations, Re⊆DPr×DPr. If, for any e∈Env,e⇒αre′ and (P,Q)∈Re, the following conditions are satisfied: (1)
IfP→α[p]P′, then there exists Q′∈DPr such that Q→α[q]Q′, max⁡{|p-r|,|q-r|,|p-q|}≤λ, and (P′,Q′)∈Re′.(2)
IfQ→α[q]Q′, then there exists P′∈DPr such that P→α[p]P′, max⁡{|p-r|,|q-r|,|p-q|}≤λ, and (P′,Q′)∈Re′.Then we call Re  λ-probabilistic bisimulation. P and Q are said to be λ-probabilistic bisimilar on the environment e if λ-probabilistic bisimulation Re exists such that (P,Q)∈Re.Proposition 27.
Letɛ=(Env,Act,⇒) be a probabilistic environment transition system. Consider λ∈[0,1]. R is an Env-indexed family of binary relations; Re⊆DPr×DPr:(1)
IfR is a parameterized probabilistic bisimulation, then, for e∈Env, Re is 0-probabilistic bisimulation.(2)
Fore∈Env, Re is λ-probabilistic bisimulation if and only if so is Re-1.(3)
Fore∈Env, Rei is a λi-probabilistic bisimulation (i=1,2); then Re1∘Re2 is a max{λ1,λ2}-probabilistic bisimulation.(4)
Fore∈Env, Rei (i∈I, where I is indexed set) is λ-probabilistic bisimulation and so is ⋃i∈IRei.Definition 28.
Letɛ=(Env,Act,⇒) be a probabilistic environment transition system. Consider λ∈[0,1]. R is an Env-indexed family of binary relations, Re⊆DPr×DPr; we define (18)~epr,λ=⋃Re∣Reisλ-probabilistic bisimulation.IfP and Q are said to be λ-probabilistic bisimilar on the environment e, then λ-probabilistic bisimulation Re exists such that (P,Q)∈Re. Thus, we can write P~epr,λQ.Proposition 29.
Consider
(1)~epr,λ forms a sequence of successively larger relations; that is, λ≤λ′ implies ~epr,λ⊂~epr,λ′.
(2)~epr,0=⋂λ>0~epr,λ; ~epr,0 coincides with the parameterized probabilistic bisimulation.Example 30.
Letɛ, P, and Q be given in Figure 6. The Env-indexed family R is shown as follows: (19)Re0=P0,Q0,Re1=P1,Q1,P2,Q2,P1,Q2,Re2=P2,Q2,Re3=P3,Q3,P3,Q5,Re4=P4,Q4,P4,Q6.Figure 6
P
0 and Q0 are 0.3-probabilistic bisimulation on the environment e0.Then we can obtain thatP0~e0pr,0.3Q0, P1~e1pr,0.3Q1, P1~e1pr,0.3Q2, P2~e2pr,0.3Q2, but P2≁e1pr,0.3Q2.Theorem 31.
Letɛ=(Env,Act,⇒) be a probabilistic environment transition system; λ∈[0,1]:(1)
IfP~epr,λQ, then α·P~α·epr,λα·Q.(2)
Iff is isomorphism mapping on Act and P~epr,λQ, then P[f]~f(e)pr,λQ[f].(3)
IfP~epr,λQ and R~fpr,λT, then pP+(1-p)R~pe+(1-p)fpr,λpQ+(1-p)T.Proof.
(1) It only needs to show there isEnv-parameterized probabilistic bisimulation R; Rα·e is λ-probabilistic bisimulation such that (α·P,α·Q)∈Rα·e. Since P~epr,λQ, Env-parameterized probabilistic bisimulation S exists such that (P,Q)∈Se. Then, we construct Env-parameterized probabilistic bisimulation R which is defined as that Rα·e={(α·P,α·Q)∣(P,Q)∈Se}, for any other e∈Env, Re=Se. Thus, we need to prove that Rα·e is λ-probabilistic bisimulation. In fact, according to Definition 23, we have that α·e⇒α[1]e, α·P⇒α[1]P, and α·Q⇒α[1]Q. And (P,Q)∈Se=Re, max⁡{|1-1|}=0≤λ. So, Rα·e is a λ-probabilistic bisimulation.
(2)Env-parameterized probabilistic bisimulation R must be presented, and Rf(e) is λ-probabilistic bisimulation such that (P[f],Q[f])∈Rf(e). In fact, since P~epr,λQ, Env-parameterized probabilistic bisimulation S exists and Se is λ-probabilistic bisimulation such that (P,Q)∈Se. Then, we establish Env-parameterized probabilistic bisimulation R, defined as Rf(e)={(P[f],Q[f])∣(P,Q)∈Se}, Re=Se. Then, Rf(e) must be proved to be λ-probabilistic bisimulation.
In fact, iff(e)⇒αrf(e′), then e⇒β[r]e′ and α=f(β). If Pf→αpP′, then P→β[p]P′′ and P′=P′′[f], α=f(β). Since (P,Q)∈Se, Q′′∈DPr exists such that Q→β[q]Q′′, and (P′′,Q′′)∈Se′ and max{|r-p|,|r-q|,|p-q|}≤λ. Furthermore, according to Definition 23, we can obtain that Qf→αqQ′′[f]=Q′, and (P′′[f],Q′′[f])∈Rf(e′). Thus, Rf(e) is λ-probabilistic bisimulation, so P[f]~f(e)pr,λQ[f].
(3) We need to determineEnv-parameterized probabilistic bisimulation R; Rpe+(1-p)f is λ-probabilistic bisimulation such that (pP+(1-p)R,pQ+(1-p)T)∈Rpe+(1-p)f. In fact, since P~epr,λQ, R~fpr,λT, so there are Env-parameterized S1 and S2 such that (P,Q)∈Se1, (R,T)∈Sf2. Next, new Env-parameterized probabilistic bisimulation R is defined as Rpe+(1-p)f={(pP+(1-p)R,pQ+(1-p)T)∣(P,Q)∈Se1and(R,T)∈Se2}, Re=Se1, and Rf=Sf2.
Ifpe+1-pf⇒αre′, then, according to Definition 23, two cases exist.
Case 1 (
e
⇒
α
[
m
]
e
′
and
r
=
p
m
). If pP+1-pR→αhP′, then P→α[l]P′ or R→α[v]P′ and h=pl or h=(1-p)v. When P→α[l]P′, since (P,Q)∈Se1, so there is Q∈DPr such that Q→α[k]Q′ and max{|l-m|,|k-m|,|k-l|}≤λ, and P′,Q′∈Se′1=Re′. So, according to Definition 23, we can get pQ+1-pR→αpkQ′ and max{|h-r|,|pk-r|,|h-pk|}=pmax{|l-m|,|k-m|,|l-k|}≤pλ≤λ and (P′,Q′)∈Se′1=Re′. When R→α[v]P′, then since (R,T)∈Se2, there exists T′∈DPr such that T→α[u]T′ and (P′,T′)∈Sf′2 and max{|v-m|,|v-u|,|u-m|}≤λ. According to Definition 23, we can obtain that pQ+1-pT→α1-puT′, so max{|(1-p)u-pm|,|h-pm|,|(1-p)u-h|}=max{|(1-p)u-pm|, |(1-p)v-pm|,|(1-p)u-(1-p)v|}≤λ, and (P′,T′)∈Sf′2=Rf′.
Case 2 (there is
f
⇒
α
[
m
]
f
′
and
r
=
(
1
-
p
)
m
). It is similar to Case 1.Notice that we do not show the proof of the substitutivity law of the synchrony operator× and restrict operator ↾. The main reason is that we can not find a suitable λ-ɛ-parameterized probabilistic bisimulation according to Definition 24. Therefore, our model only uses prefix operator α, relabeled operator [f], and sum operator ∑‍ to help us verify the approximate correctness. In the future, I will attempt to find a suitable model to support the substitutivity law.


## 6. Conclusion

In this study, we formalized the approximate correctness of software products. We focused on the approximate version of parameterized bisimulation and extended parameterized bisimulation to probabilistic settings. We presented the definitions ofλ-parameterized bisimulation and λ-parameterized probabilistic bisimulation over the environment e. These approximate versions provide theoretical foundations to verify the degree to which the software is approximately correct. In the future, we will try to find some effective algorithms to realize the verification. The substitutivity laws of λ-parameterized bisimulation over the environment e and λ-parameterized probabilistic bisimulation over the environment e are presented.The modal logical characterizations ofλ-parameterized bisimulation and λ-parameterized probabilistic bisimulation over the environment e are useful to verify whether or not two processes are approximate under parameterized bisimulation. In the future, we will attempt to establish the modal logical descriptions of λ-parameterized bisimulation and λ-parameterized probabilistic bisimulation.



---

*Source: 173012-2015-07-16.xml*