Approximate trace and singleton failures equivalences for transition systems

Chao Wang,Jinzhao Wu,and Hongyan Tan

1.Schoolof Computer and Information Technology,Beijing Jiaotong University,Beijing 100044,China;

2.Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities,Nanning 530006,China;

3.Institute of Acoustics,Chinese Academy of Sciences,Beijing 100190,China

Approximate trace and singleton failures equivalences for transition systems

Chao Wang1,Jinzhao Wu2,*,and Hongyan Tan3

1.Schoolof Computer and Information Technology,Beijing Jiaotong University,Beijing 100044,China;

2.Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities,Nanning 530006,China;

3.Institute of Acoustics,Chinese Academy of Sciences,Beijing 100190,China

Established system equivalences fortransition systems, such as trace equivalence and failures equivalence,require the observations to be exactly identical.However,an accurate measurementis impossible when interacting with the physicalworld,hence exact equivalence is restrictive and not robust.Using Baire metric,a generalized framework of transition system approximation is proposed by developing the notions of approximate language equivalence and approximate singleton failures(SF)equivalence. The framework takes the traditionalexactequivalence as a special case.The approximate language equivalence is coarser than the approximate SF equivalence,just like the hierarchy of the exact ones.The main conclusion is that the two approximate equivalences satisfy the transitive property,consequently,they can be successively used in transition system approximation.

approximate equivalence,trace,singleton failures (SF),transition systems.

1.Introduction

The term system equivalence is the notion that a component of a system behaves in a similar way as a component of a different system,where similarity means that the components will be mathematically indistinguishable from each other.The system equivalence is used to simplify complex systems in the specification and verification of the behaviourof systems.

Van Glabbeek studied various semantic equivalences in the linear time-branching time spectrum[1],which is applied to finitely branching,concrete and sequentialprocesses.Finitely branching means a process in each state has only finitely many possible ways to proceed,concrete means a process does not have internal actions,and sequentialmeans a process can perform atmostone action at a time.Note thata process may be non-deterministic(i.e., after a trace,a process may arrive at different states)and may have infinite length traces.

This paperinvestigates the same range ofprocesses with [1],and only focuses on the following two canonical semantics,which are respectively representatives of linear time semantics and branching time semantics.

(i)Trace semantics,which is the coarsest semantics as presented in[2].

(ii)Singleton failures(SF)semantics,which applies in general to asynchrously communicating processes as observed firstly in[3].Its denotationalsemantics forcommunicating sequentialprocesses(CSP)was defined in[4].

Trace semantics is very importantand a lot of research has been carried outon it.As a variantoffailures semantics [5],SF semantics is also very important,since failures semantics has wide applications.For example,Kennaway’s equivalence[6]and testing equivalence[7]were shown to coincide with the failures equivalence on the domain of finitely branching and concrete transition systems in[8]. Reference[9]developed a framework of timed equivalences for timed event structures,and used trace,testing and bisimulation[10]as standard equivalences.Reference [11]did research on explicitrepresentation of the termination in CSP while itused traces,stable failures and failuresdivergences as standard denotational models of CSP.Reference[12]introduced the concept of a distributed reactive system which works with two semantic equivalences, namely a variant of failures equivalence and a variant of bisimulation equivalence.

SF semantics distinguishes between pairs of processes that would be identified in trace semantics,yet identifies others that would be distinguished in bisimulation semantics.SF semantics and bisimulation semantics are representatives of branching time semantics,however the complexity of SF semantics versus bisimulation semantics is similar to thatofpolynomialversus nondeterministic polynomial.Different from failures semantics,the refusal set of SF pairs must contain one and only one element and thus easy to handle.In sum,this paper uses SF semantics instead of bisimulation semantics as a representative of branching time semantics.

Based on previous researches[1],the set of all traces and SF pairs is used to characterize SF equivalence.We give a common example to illustrate that the trace information cannot be obtained from the set of all SF pairs, hence the set of all SF pairs alone cannot characterize the SF equivalence.Then we propose a revised version of singleton failure(RSF)pair and show thatthe set of all RSF pairs alone can characterize the SF equivalence.Furthermore,the RSF algorithm gains in efficiency in terms of speed than the traditionalSF algorithm by reducing redundancy elements,while retaining the same information content.

Currently,established system equivalences for transition systems,such as trace equivalence and failures equivalence,require the observations to be exactly identical. However,an accurate measurementis impossible when interacting with the physical world,hence the usual exact equivalence is quite restrictive and notrobust.

The notion of distance between the original transition system and the targettransition system is much more adequate in this context.Instead of requiring the observations of the two transition systems to be equal,the distance between them is only required to remain bounded by some parameter called precision of the approximation.This approach notonly defines more robustrelationsbetween transition systems butalso allows more significantcomplexity reduction.

Using Baire metric[1],this paper proposes a generalized framework of transition system approximation including approximate language equivalence and approximate SF equivalence.In addition,the exact language equivalence and the exactSF equivalence are specialcases of approximate language equivalence and approximate SF equivalence,respectively.Approximate language equivalence is coarser than approximate SF equivalence,the two approximate equivalences have the same hierarchy as the exact ones.We define and calculate language(or SF)distance between pairs of transition systems,and show that the sets of transition systems together with language(or SF)distance form a pseudo-metric space.

The unique feature ofthe two approximate equivalences is that they satisfy the transitive property.Hence,for an originalcomplex system,we can successively use the two approximate equivalences to obtain an equivalent system with lesser complexity.Therefore the two approximate equivalences would be very usefulfordevelopers of model checking tools.

2.Preliminaries

The following notations are used throughoutthe paper.N denotes the set of all natural numbers(including zero),R denotes the set of all real numbers,and?denotes the empty set.For l,l∈R,ldenotes the round-down of l,which is the largest integer less than or equal to l, max(l,l?)denotes the larger one of l and l?.For a setΠ, Π∞denotes both finite and infinite sequences overΠ.

Definition 1A pseudo-metric space is a setΠtogether with a function d:Π×Π→[0,+∞](called a pseudometric)such that,?x,y,z∈Π,

(i)d(x,x)=0;

(ii)d(x,y)=d(y,x)(symmetry);

(iii)d(x,z)?d(x,y)+d(y,z)(triangular inequality).

Hence,a pseudo-metric space is a metric space in which the distance between two distinct points can be zero.In other words,d(x,y)=0 does notalways imply x=y.

Definition 2The Baire metric dB:Π∞×Π∞→[0,1] is defined by

where l∈N is the length of the longestcommon prefix of ρ1∈Π∞andρ2∈Π∞.

For brevity,ifρ1=ρ2,we define l=+∞no matter whatthe length ofρ1.

Itis easy to verify that(Π∞,dB)is a metric space and dB(ρ1,ρ2)measures the similarity betweenρ1andρ2,the lower the value,the more similar the two sequences.

The infimum(or supremum)of a subset S of realnumbers is denoted by inf(S)(or sup(S))and is defined to be the biggest(or least)real number which is smaller(or greater)than orequalto allnumbers in S.

Definition 3LetΠ1?Π,Π2?Π,the Hausdorff distance associated with d,which is a pseudo-metric onΠ,is defined by

The most important property of the Hausdorff distance is thatthe Hausdorff distance associated with any pseudometric onΠis a pseudo-metric on the setof subsets ofΠ.Informally,two non-empty subsets of a matric space are close in their Hausdorff distances,if every point of either subset is close to some point of the other subset.In other words,the Hausdorff distance dHis the greatest of all the distances from a pointin one subsetto the closest pointin the other subset.Hence,the Hausdorff distance is used to measure the distance(or similarity)between pairs of differentsets.

Itis easy to prove that dH(Π1,Π2)=0 iff(if and only if)cl(Π1)=cl(Π2),where cl(Π1)and cl(Π2)denote the topologicalclosures ofΠ1,Π2respectively.Moreover,dHis a pseudo-metric.

Definition 4A labelled transition system with observations is a six-tuple T=(Q,Σ,→,Q0,Π,〈.〉),where Q is a(possibly infinite)set of states;Σis a(possibly infinite)set of labels;→?Q×Σ×Q is a setof transitions; Q0?Q is a(possibly infinite)setof initialstates;Πis a (possibly infinite)set of observations;〈.〉:Q→Πis an observation map.

If no confusion arises,the transition system will be referred to as the labelled transition system.

3.Approximate language equivalence

Firstly,we introduce the definitions of trace,state trajectory,externaltrajectory and the language oftransition systems.Secondly,we depict the distance between pairs of external trajectories and deduce the language distance between pairs of transition systems.Hence,transition systems together with the language distance form a pseudometric space.Finally,we define thattwo transition systems have an approximate language relation if they are“close”according to the language distance,and prove thatthe approximate language relation is an equivalence relation.

In the remainder of this paper,let T=(Q,Σ,→, Q0,Π,〈.〉)be a transition system with observations, (qi,ai+1,qi+1)∈→,i=0,1,2,...and q0∈Q0.

A trace of T is a(possibly infinite)sequence of labels α=a1a2....

A state trajectory of T is a(possibly infinite)sequence

An external trajectory of T is a(possibly infinite)sequence of elements ofΠ×Σ×Π,ψ=〈q0〉a1〈q1〉a2〈q2〉....

Since the trace,state trajectory and external trajectory are similar,we only discuss the external trajectory for brevity,it is obvious that our approximation method also works for trace and state trajectory.

The set of allexternal trajectory of T is called the language of T,and is denoted by L(T).

By convention,a transition(q,a,q?)∈→is denoted byWrite o for the empty sequences ofexternaltrajectories,ψ1ψforthe concatenationrecursively by

The remaining partofthis section is devoted to approximate language equivalence.Atthe very beginning,the traditionalexactlanguage equivalence is given as follows.

Definition 5Two transition systems T1and T2are language equivalent,in other words,there is a language equivalence relation between T1and T2,notation T1=LT2,iff L(T1)=L(T2).

Definition 6The distance dψ:L(T1)×L(T2)→[0,1] between pairs of externaltrajectoriesψ1andψ2is defined by ?

where l∈N is the length of the longestcommon prefix of ψ1andψ2.

This definition is a generalization of the Baire metric (Definition 2)for externaltrajectories.The following is an easy observation.

Theorem 1?ψi∈L(Ti),i=1,2,3,dψ(ψ1,ψ3)? max(dψ(ψ1,ψ2),dψ(ψ2,ψ3)).

ProofIfψ1=ψ2orψ2=ψ3,then the right-hand side of the inequality is equalto the left-hand side.Hence,the inequality trivially holds.

Ifψ1=ψ3,then the left-hand side of the inequality is equalto 0.Hence,the inequality holds.

Otherwise,ψ1/=ψ2,ψ2/=ψ3andψ1/=ψ3.Let l∈N be the length of the longestcommon prefix ofψ1andψ2, and l?∈N be the length of the longestcommon prefix of ψ2andψ3.Withoutloss of generality,assume l?l?,then the length ofthe longestcommon prefix ofψ1andψ3is no less than l.

Hence,dψ(ψ1,ψ3)?max(dψ(ψ1,ψ2),dψ(ψ2,ψ3)) holds in allcases.

The following theorem shows that the definition of dψis reasonable,i.e.,the distance is a pseudo-metric.

Theorem 2dψis a pseudo-metric on the setofexternal trajectories.

ProofLetψ1,ψ2,ψ3be arbitrary externaltrajectories. dψ(ψ1,ψ2)≥0,dψ(ψ1,ψ1)=0.

(i)Firstly,we prove that dψ(ψ1,ψ2)=dψ(ψ2,ψ1) (symmetry).

Ifψ1=ψ2,then dψ(ψ1,ψ2)=0=dψ(ψ2,ψ1).Other-wise,dψ(ψ1,ψ2)=dψ(ψ2,ψ1),where l∈N is the length of the longest common prefix ofψ1andψ2. Hence,dψ(ψ1,ψ2)=dψ(ψ2,ψ1)holds in allcases.

(ii)Second,we prove that dψ(ψ1,ψ3)?dψ(ψ1,ψ2)+ dψ(ψ2,ψ3)(triangularinequality). By Theorem 1,

Consequently,dψis a pseudo-metric.

Furthermore,the metric dψo(hù)n the setof externaltrajectories induces a naturallanguage distance between pairs of transition systems.

Definition 7The language distance between T1and T2is defined by dL(T1,T2)=dH(L(T1),L(T2)).

Since the Hausdorffdistance is pseudo-metric,the definition of the language distance is reasonable.Hence,transition systems together with the language distance form a pseudo-metric space.

The intuitive meaning of the language distance is the following.For any external trajectory of T1,we can find an externaltrajectory of T2such thatthe distance between them remains bounded by dL(T1,T2).

Example 1Consider the transition systems of T1,T2and T3in Fig.1,where the firsttwo transition systems are taken from counter Example 5 in[1].

Fig.1 A complex case

dL(T1,T2)=0 intuitively means that for any external trajectory of T1(or T2),we can find an externaltrajectory of T2(or T1)such thatthe two executions are indistinguishable to an external observer,in other words,they have the same observations.

dL(T2,T3)=2?3intuitively means that for any externaltrajectory of T2(or T3),we can find an externaltrajectory of T3(or T2),such that from the view of an external observer,they are indistinguishable from the firstthree observations.

One of the great advantages of having metric structure on transition systems is that the distance enables us to use quantitative approximation.

Definition 8Two transition systems T1and T2are approximate language equivalent with the precisionξ≥0, in other words,there is an approximate language relation?L,ξbetween T1and T2,notation T1?L,ξT2,iff dL(T1,T2)?ξ.

It is intuitive that the lower the value ofξ,the higher the degree to which?L,ξis a language relation.It should be emphasized thattwo transition systems are approximate language equivalent with the precisionξ=0,which is also known as they are exactlanguage equivalent.In other words,the traditionalexactlanguage equivalence is a special case(ξ=0)of approximate language equivalence. Hence,Definition 8 is a generalization of Definition 5.

Theorem 3?L,ξ(ξ≥0)is an equivalence relation on the setof transition systems.

ProofLet T1,T2,T3be arbitrary transition systems.

(i)First,we prove that?L,ξis a reflexive relation. dL(T1,T1)=dH(L(T1),L(T1))=0?ξ,thus,T1?L,ξT1.

(ii)Second,we prove that?L,ξis a symmetric relation. Since dψand max are symmetric,we have the following equation:

Assume T1?L,ξT2,then dL(T2,T1)=dL(T1,T2)? ξ,namely,T2?L,ξT1.Hence,?L,ξis a symmetric relation.

(iii)Third,we prove that?L,ξis a transitive relation.

Assume T1?L,ξT2and T2?L,ξT3.

?ψ1∈L(T1),by(1),?ψ2∈L(T2)such that dψ(ψ1,ψ2)?ξ.

Forψ2,by(2),?ψ3∈L(T3)such that dψ(ψ2,ψ3)?ξ.

By Theorem 1,

This formula holds forallψ1∈L(T1). Hence,

Consequently,?L,ξis a transitive relation.?

Example 2Consider again the transition systems in Example 1.Since dL(T1,T2)＜0.125,T1?L,0.125T2. Since dL(T2,T3)=0.125,T2?L,0.125T3.By Theorem 3, T1?L,0.125 T3.

4.Approximate SF equivalence

Firstly,we introduce the definitions of SF pair,failure pair and Kennaway pairoftransition systems.Secondly,we depictthe distance between pairs of SF pairs by extending the definition ofthe Baire metric,and deduce the SF distance. Therefore,transition systems togetherwith the SF distance form a pseudo-metric space.Finally,we define that two transition systems have an approximate SF relation if they are“close”according to the SF distance,and we prove that this approximate SF relation is an equivalence relation.

The setofnextactions of a state q is defined by N(q)= {a∈Σ|?q?∈Q such that(q,a,q?)∈→}.

(ψ,π)is an SF pair of T,whereψis an externaltrajectory andπis a singleton refusalaction,if?q0∈Q0,q∈Q such that q=ψ?q andπ∈/N(q).

0

(ψ,D)is a failure pair of T,if?q0∈Q0,q∈Q such that q=ψ?q and D∩N(q)=?where D?Σ(note that

0??Σ,namely,D can be?).

(ψ,D)is a Kennaway’s pair[10]of T,if?q0∈Q0,q∈Q such that q=ψ?q and D∩N(q)/=?where D?Σ.

0

Since the SF pair,failure pair and Kennaway’s pair are similar,we only analyze the SF pair for brevity,it is obvious that our approximation method also works for the failure pair and the Kennaway’s pair.

The definition of the SF pair presented here is that of [1].Itdiffers from thatof[4]in one importantrespect,the refusalsetofthe SF pairmustcontain one element,instead of atmostone element.

Let F?(T)denote the setofall SF pairs of T.The traditionalexact SF equivalence is given as follows.

Definition 9Two transition systems T1and T2are SF equivalent,in other words,there is an SF equivalence relation between T1and T2,notation T1=FT2,iff F?(T1)= F?(T2)and L(T1)=L(T2).

Example 3Fig.2 considers T0with justone node p and a self-loop action from and to thatnode labelled a.F?(T0) is the empty setforitis neverpossible to refuse any action. T1firstdoes an action a and then reaches either the node p or deadlock 0.Therefore,F?(T1)=F?(T2).Yet,L(T1)is notequalto L(T2).

Fig.2 F'(T)and L(T)

This example illustrates that F?(T)does not imply L(T),hence F?(T)alone cannot characterize SF equivalence.Then we propose an RSF pair and show that the set of all RSF pairs alone can characterize SF equivalence.Furthermore,the RSF algorithm gains in efficiency in terms of speed than the traditional SF algorithm by reducing redundancy elements,while retaining the same information content.

Here we present the basic definitions.For an external trajectoryψo(hù)f T,the set of all possible actions is de-fined by Cont(T,ψ)={a∈Σ|?q0∈Q,q,q∈Q such that q0=ψ?q and(q,a,q?)∈→}.

|ψ|denotes the length ofψ.ψwill be denoted by |ψ|=+∞ifψhas infinite length.The maximum length of the language of T1and T2is defined by Len(T1,T2)= max(ψm∈La(xT)|ψ1|,ψm∈La(xT)|ψ2|).

1122

∈denotes the zero-length actions.In order to make the external trajectory and the SF pair have the same form,ψ is identified with a pair(ψ,∈)in this paper.

Definition 10(ψ,π)is an RSF pair of T if?q0∈Q0,q∈Q such that

Let F(T)denote the setof all RSF pairs of T.

F(T)has the following two advantages.Firstly,F(T) is easy to calculate,since the definition of the RSF pair only involves N(q)and Cont(T,ψ).Secondly,F(T)removes the following two classes of elements from L(T)∪F?(T),

(i)(ψ,∈)∈L(T)where Cont(T,ψ)/=?∧|ψ|/=+∞.

(ii)(ψ,π)∈F?(T)whereπ/∈Cont(T,ψ).

In order to prove that the set of all RSF pairs alone can characterize SF equivalence,namely,T1=FT2iff F(T1)=F(T2)(Theorem 4).We firstly prove that F(T) is the subsetof the union of L(T)and F?(T)(Lemma 1). Secondly,we prove thatiftransition systems have the same F(T),they have the same L(T)(Lemma 2).Thirdly,we prove that if transition systems have the same F(T),they have the same F?(T)(Lemma 3).

Lemma 1F(T)?L(T)∪F?(T).

Proof?(ψ,π)∈F(T),we shallprove that(ψ,π)also belongs to L(T)∪F?(T).

Since(ψ,π)∈F(T),?q0∈Q0,q∈Q such that

Case 1π=∈.Hence(ψ,∈)∈L(T).

Case 2π∈Cont(T,ψ)∧π∈/N(q).Hence(ψ,π)∈

In both cases,(ψ,π)∈L(T)∪F?(T).

Informally,F(T)is a smallerversion of L(T)∪F?(T), itreduces redundancy elements which can be derived from the otherelements.

Lemma 2F(T1)=F(T2)?L(T)=L(T2).

ProofBy contradiction,assume that L(T)/=L(T2). Since T1and T2are symmetric,we assume there is an element(ψ,∈)which belongs to L(T1)and does not belong to L(T2).

If Cont(T1,ψ)is the empty set.By the definition of the RSF pair,(ψ,∈)∈F(T1).Since F(T1)=F(T2), (ψ,∈)∈F(T2).By Lemma 1,F(T2)?L(T2)∪F(T2), (ψ,∈)∈L(T2)∪F?(T2).By the definition of the SF pair, (ψ,∈)∈/F?(T2).Hence(ψ,∈)∈L(T2),which contradicts the assumption(ψ,∈)∈/L(T2).

Otherwise,Cont(T1,ψ)is not an empty set.Hence?a∈Cont(T1,ψ).As(ψ,∈)∈L(T1),?q∈Q such that (ψa〈q〉,∈)∈L(T1).Since(ψ,∈)∈/L(T2),(ψa〈q〉,∈)∈/ L(T2).Sinceψa〈q〉is longer thanψ,using the recursive method,there is an infinite length element(ψ?,∈)which belongs to L(T1)and does not belong to L(T2).By the definition of the RSF pair,(ψ?,∈)∈F(T1)and(ψ?,∈)∈/ F(T2),which contradicts the premise F(T1)=F(T2).

Hence,L(T1)/=L(T2)has been shown impossible, L(T1)=L(T2)mustbe true.

Lemma 3F(T1)=F(T2)?F?(T1)=F?(T2).

ProofBy contradiction,assume that F?(T1)/=F?(T2). Since T1and T2are symmetric,we assume there is an element(ψ,π)which belongs to F?(T1)and does notbelong to F?(T2).

Since(ψ,π)∈F?(T1),?q0∈Q0,q∈Q such that q=ψ?q,π∈/N(q).This implies that(ψ,∈)∈L(T).

1Since F(T1)=F(T2),by Lemma 2,L(T1)=L(T2). Then,(ψ,∈)∈L(T2).

Ifπ∈Cont(T1,ψ),(ψ,π)∈F(T1).Since F(T1)= F(T2),(ψ,π)∈F(T2).By Lemma 1,F(T2)?L(T2)∪F?(T2),(ψ,π)∈L(T2)∪F?(T2).Since(ψ,π)∈/ L(T2),(ψ,π)∈F?(T2),which contradicts the assumption (ψ,π)∈/F?(T2).

Otherwiseπ∈/Cont(T1,ψ)and L(T1)=L(T2), π∈/Cont(T2,ψ).Since(ψ,∈)∈L(T2),(ψ,π)∈F?(T2), which contradicts the assumption(ψ,π)∈/F?(T2).

Hence,F?(T1)/=F?(T2)has been shown impossible, F?(T1)=F?(T2)mustbe true.

Theorem 4T1=FT2iff F(T1)=F(T2).

ProofNow we prove that L(T1)=L(T2)∧F?(T1)= F?(T2)iff F(T1)=F(T2).

To prove the sufficiency,by contradiction,assume that F(T1)/=F(T2).Since T1and T2are symmetric,we assume there is an element(ψ,π)which belongs to F(T1) and does notbelong to F(T2).

Thenπfalls into one of the following two cases:

Case 1π=∈.Namely,(ψ,∈)∈F(T1).By the definition of the RSF pair,one of the following two cases must hold:

Case 1A Cont(T1,ψ)=?.Since L(T1)=L(T2), Cont(T2,ψ)=?.Hence(ψ,∈)∈F(T2),which contradicts the assumption(ψ,∈)∈/F(T2).

Case 1B|ψ|=+∞.Since(ψ,∈)∈L(T1)and L(T1)=L(T2),(ψ,∈)∈L(T2).Hence(ψ,∈)∈F(T2), which contradicts the assumption(ψ,∈)∈/F(T2).

Case 2π/=∈.By the definition of the RSF pair,?q0∈Q0,q∈Q such that q0=?q andπ∈/ N(q).Hence(ψ,π)∈F?(T1).Since F?(T1)=F?(T2), (ψ,π)∈F?(T2).Namely,?q0?∈Q0,q?∈Q,such that q0?=ψ?q?,π∈/N(q?).Since(ψ,π)∈F(T1),π∈Cont(T1,ψ).Since L(T1)=L(T2),π∈Cont(T2,ψ). Consequently,(ψ,π)∈F(T2),which contradicts the assumption(ψ,π)∈/F(T2).

Hence,F(T1)/=F(T2)has been shown impossible, F(T1)=F(T2)mustbe true.

To prove the necessity,by Lemma 2,L(T1)=L(T2). By Lemma 3,F?(T1)=F?(T2).

Example 4Consider again T1and T2in Example 1. In order to verify whether T1and T2are SF equivalent,it needs 46 comparisons when using the SF algorithm,while itneeds 8 comparisonswhen using the RSF algorithm.The RSF algorithm reduces 82.6%workload in this complex case.

Example 5Consider T4and T5in Fig.3.In order to verify whether T4and T5are SF equivalent,itneeds atleast six comparisons when using the traditional SF(namely, L(T)∪F?(T))algorithm,while it only needs 1 comparison when using the RSF(namely,F(T))algorithm. The RSF algorithm reduces 83.3%workload in this simple case.

Fig.3 A simple case

Note thatitis noteffective to use the method described above to prove that two transition systems are SF equivalentby enumerating their RSF pairs,since these RSF pairs are usually infinitely many.The enumeration is only used to obtain a comparison result.

The following definition is a generalization of Definition 6 for SF pairs.

Definition 11The distance df:(L(T1),Π1)× (L(T2),Π2)→[0,1]between SF pairs(ψ1,π1)and (ψ2,π2)is defined by

where l∈N is the length of the longest common prefix ofψ1andψ2.If Len(T1,T2)is finite,thenγ=Otherwise,γis an infinitesimalnumber,namely,?k∈N,γ＜2?k.

The following is an easy observation.

Theorem 5?ψi∈L(Ti),πi∈Πi,i=1,2,3,

ProofLet l∈N be the length of the longestcommon prefix ofψ1andψ2,l?∈N be the length of the longestcommon prefix ofψ2andψ3,and l∈N be the length of the longestcommon prefix ofψ1andψ3.

(i)Ifψ1=ψ3andπ1=π3,df((ψ1,π1),(ψ3,π3))=0. Hence,the inequality holds. (ii)Ifψ1=ψ3andπ1/=π3.

Ifψ1=ψ2,then eitherπ2/=π1orπ2/=π3mustbe true.

Otherwise,ψ1/=ψ3.

Ifψ1=ψ2,then l??=l?andψ2/=ψ3.

Ifψ2=ψ3,itis similar to the above caseψ1=ψ2.

Otherwise,ψ1/=ψ3,ψ1/=ψ2andψ2/=ψ3,without loss ofgenerality,assume l?l?,then we have l??≥l.

The following theorem shows thatthe definition of dfis reasonable.

Theorem6dfis a pseudo-metric on the setof SF pairs.

The proof is omitted since it is similar to the proof of Theorem 2.

Furthermore,the metric dfon the set of SF pairs naturally induces an SF distance between pairs of transition systems.

Definition 12The SF distance between T1and T2is defined by dF(T1,T2)=dH(F(T1),F(T2)).

Since the Hausdorff distance is a pseudo-metric,the definition of the SF distance is reasonable.Hence,transition systems togetherwith the SF distance form a pseudometric space.

The intuitive meaning of the SF distance is as follows. For any SF pair of T1,we can find an SF pair of T2such that the distance between them remains bounded by dF(T1,T2).

Definition 13Two transition systems T1and T2are approximate SF equivalentwith the precisionξ≥0,in other words,there is an approximate SF relation?F,ξbetween T1and T2,notation T1?F,ξT2,iff dF(T1,T2)?ξ.

Itis intuitive thatthe lower the value ofξ,the higherthe degree to which?F,ξis an SF relation.It should be emphasized that two transition systems are approximate SF equivalentwith the precisionξ=0,which is also known as they are exact SF equivalent.In other words,the traditional exact SF equivalence is a special case(ξ=0)of approximate SF equivalence.Consequently,Definition 12 is a generalization of Definition 9.

Theorem 7?F,ξ(ξ≥0)is an equivalence relation on the setof transition systems.

The proof is omitted since it is similar to the proof of Theorem 3.

5.Hierarchy of equivalences

In this section,we show thatthe language distance between two transition systems is notgreaterthan their SF distance. A direct consequence is that if two transition systems are approximate SF equivalentwith a precisionξ,then they are approximate language equivalent withξ.In other words, approximate language equivalence is coarser than the approximate SF equivalence,hence these approximate equivalences have the same hierarchy as the exact ones in the lineartime-branching time spectrum[1].Theorem 8dL(T1,T2)?dF(T1,T2)ProofBy the definition of SF,

By definitions of the distance dfand the distance dψ, Now,we assume that{df((ψ1,∈),(ψ2,π2))|(ψ2, π2)∈F(T2)}reaches the minimum when(ψ2,π2)=by the definition of SF,

Traditionally,T1=FT2implies T1=LT2.A similar conclusion is reached as follows.

Corollary 1T1?F,ξT2implies T1?L,ξT2.

Hence,the approximate language equivalence is coarser than the approximate SF equivalence,and the two approximate equivalences have the same hierarchy as the exact ones.

6.Cases study

Two cases are investigated in this section.The firstcase is simple,butnottrivial,as itillustrates thatthe approximate language equivalence and the approximate SF equivalence can be successively used to achieve complexity reduction in the approximation process.The second case illustrates that different error limits may result in different relations between transition systems,in other words,we can define more robustrelations between transition systems.

It is convenient to describe transition systems by directed graphs.Each state is represented by a circle,the observation is shown inside the circle,and a transition from one state to another is indicated by an arrow with a label.

A microwave and lightwave oven is a kitchen appliance that heats food using microwaves and lightwaves.We use a transition system to characterize the process ofcooking a pizza in a microwave and lightwave oven.There are different transition systems for different processes of cooking a pizza.The observationsconsistofinitial,microwave heating,lightwave heating and final,which are respectively abbreviated as i,a,b and f.Hence,the setof observations

Π={i,f,a,b}.We use label1 to denote a 5-minute heating and label0 to denote no heating.Consequently,the set of labelsΣ={0,1}.

6.1 Transitive property

Fig.4 depicts that a microwave and lightwave oven takes

20 minutes(microwave heating)ortakes 15 minutes(lightwave heating)to cook a pizza.Similarly,Fig.5 depicts thata microwave and lightwave oven takes 10 minutes(microwave heating)or takes 15 minutes(lightwave heating) to cook a pizza.And Fig.6 depicts that a microwave and lightwave oven takes 10 minutes(microwave heating)or takes 10 minutes(lightwave heating)to cook a pizza.

Fig.4 T6

Fig.5 T7

We set the error limitξ=0.125,namely,we assume thatthe error0.125 is tolerable.Since the maximum length of the language of T6,T7and T8is 112?7.For more information,see Definition 11.After a straightforward calculation using the definition of SF distance(Definition 12),we obtain

Since?F,ξis an equivalence relation on the set of transition systems(Theorem 7),(8)and(9)imply that dF(T6,T8)?ξ,i.e.,T6?F,ξT8.And T6?F,ξT8implies T6?L,ξT8(Corollary 1).

By successively using approximate equivalence,we obtain T6and T8are both approximate language equivalent with the precisionξand approximate SF equivalent with the precisionξ.

Hence,we should use T8to replace T6in the specification and verification,because T8intuitively has a smaller structure than T6,and the complexity of the specification and verification is typically associated with the size of the state space.

Note thatthe transitive property plays an importantrole in ourefforts to obtain an equivalentsystem with less complexity,because the transitive property makes itpossible to successively use approximate equivalences.

6.2 Error limit

Fig.7 depicts that a microwave and lightwave oven takes five minutes(microwave heating)to cook a pizza or detects an errorand stops.Similarly,Fig.8 depicts thata microwave and lightwave oven takes five minutes(microwave heating)to cook a pizza.

Fig.7 T 9

Fig.8 T10

Since the maximum length ofthe language of T9,T10is=0.062 5.After a straightforward calculation,we obtain

If the error limitξ＜0.062 5,then T9and T10are approximate language equivalent but not approximate SF equivalent.If the error limitξ≥0.062 5,then T9and T10are both approximate language equivalentand approximate SF equivalent.In otherwords,differenterrorlimits may resultin differentrelations between T9and T10.

7.Comparison

Our version of the Baire metric is described in[13]which presents an introduction to metric semantics for programming and specification languages.In this paper,we extend the definition of the Baire metric to suit the specific requirements of externaltrajectories and SF pairs.

A metric very similar to this definition is defined by Baire in[14].The alternative version of the Baire metric is typically used to measure the similarity between strings [15,16],butitdoes notsupportTheorem 1 and Theorem 5, which are the essential precondition for the derivation of the transitive property of approximate language equivalence(Theorem 3)and approximate SF equivalence(Theorem 7).

In the pastseveraldecades,there have been a lotof researches on system approximation.Approximate trace and approximate(bi)simulation relations are studied for transition systems[17]and hybrid systems[18,19]by Girard and Pappas.Their approximation is based on a metric on the setof observations which can be any metric.However, none of their approximate relations is an equivalence relation,as they do not satisfy the transitive property.Hence, their approximate relations cannot be successively used, while our approximate equivalences do nothave this limit. For example,T1?F,ξT2,T2?F,ξT3,...,Tn?1?F,ξTnimply that T1?F,ξTn.

Previous work on SF is relatively sparse.Since the computationalcomplexity of SF is lowerthan bisimulation,this paper uses SF semantics instead of bisimulation as a representative of branching time semantics.

8.Conclusions

Using the Baire metric,this paper proposes a generalized framework of transition system approximation by developing the notions of approximate language equivalence and approximate SF equivalence.The language semantics and SF semantics are,respectively,representatives of linear time semantics and branching time semantics.The exactlanguage equivalence and the exact SF equivalence are specialcases of approximate language equivalence and approximate SF equivalence,respectively.Approximate language equivalence is coarser than approximate SF equivalence,and two approximate equivalences have the same hierarchy as the exactones.

A revised version of SF pairs is proposed to simplify SF equivalence checking,and the RSF algorithm gains in efficiency in terms of speed than the traditional SF algorithm by reducing redundancy elements,while retaining the same information content.

The motivation of the approximate equivalence is to define more robustrelations between transition systems,and to achieve a considerable complexity reduction in the approximation process.

We may be the first to give a reasonable definition of the distance between pairs of SF pairs,and deduce the SF distance between pairs of transition systems.Transition systems together with this distance form a pseudo-metric space.

The main conclusion of this paper is that the twoapproximate equivalences satisfy the transitive property, hence,they can be successively used in transition system approximation.In otherwords,we can successively use the two approximate equivalences to obtain a much more simplified equivalentsystem from an originalcomplex system. The two approximate equivalences guarantee some quality and efficiency in the specification and verification,therefore,they would be very useful for developers of model checking tools.

In the future work,we plan to develop approximate equivalences for other types of systems,such as hybrid systems and hybrid event structures.Future interests also include the computer-aided analysis software for verifying SF equivalence which stems from the RSF pair definition.

[1]R.J.Van Glabbeek.The linear time-branching time spectrum i-the semantics ofconcrete,sequentialprocesses.Handbook of Process Algebra,2001.

[2]U.Fahrenberg,A.Legay.The quantitative lineartime branching time spectrum.Theoretical Computer Science,2014,538: 54–69.

[3]F.S.de Boer,J.N.Kok,C.Palamidessi,etal.The failure of failures in a paradigm for asynchronous communication.Lecture Notes in Computer Science,1991,527:111–126.

[4]C.Bolton,J.Davies.A singleton failures semantics for communicating sequential processes.Formal Aspects of Computing,2006,18(2):181–210.

[5]S.D.Brookes,C.A.R.Hoare,A.W.Roscoe.A theory ofcommunicating sequential processes.Journal of the ACM,1984, 31(3):560–599.

[6]J.R.Kennaway.Formalsemantics ofnondeterminism and parallelism.Oxford:University of Oxford,1981.

[7]R.de Nicola,M.C.B.Hennessy.Testing equivalences forprocesses.TheoreticalComputer Science,1984,34(1):83–133.

[8]R.de Nicola.Extensional equivalences for transition systems. Acta Informatica,1987,24(2):211–237.

[9]M.V.Andreeva,I.B.Virbitskaite.Timed equivalences for timed event structures.Parallel Computing Technologies. Berlin:Springer,2005:16–26.

[10]M.V.Andreeva,I.B.Virbitskaite.Modular bisimulation theory for computations and values.Foundations ofSoftware Science and Computation Structures.Berlin:Springer,2005:16–26.

[11]S.Dunne.Termination withoutcheckmark in CSP.FM 2011: FormalMethods.Berlin:Springer,2011:278–292.

[12]R.J.Van Glabbeek,U.Goltz,J.Wolfhard,etal.On characterising distributability.Logical Methods in Computer Science, 2013,9(3):1–58.

[13]F.Van Breugel.An introduction to metric semantics:operationaland denotationalmodels forprogramming and specification languages.Theoretical Computer Science,2001,258(1): 1–98.

[14]R.Baire.Sur la reprsentation des fonctions discontinues.Acta mathematica,1906,30(1):1–48.

[15]Y.Cao,M.Ying.Similarity-based supervisory control of discrete-event systems.IEEE Trans.on Automatic Control, 2006,51(2):325–330.

[16]Y.Cao,G.Chen.Towards approximate equivalences of workflow processes.Proc.of the 1st International Conference on E-Business Intelligence,2010.

[17]A.Girard,G.J.Pappas.Approximation metrics for discrete and continuous systems.IEEE Trans.on Automatic Control, 2007,52(5):782–798.

[18]A.Girard,A.A.Julius,G.J.Pappas.Approximate simulation relations forhybrid systems.Discrete EventDynamic Systems, 2008,18(2):163–179.

[19]A.Girard,G.J.Pappas.Approximate bisimulation:a bridge between computer science and control theory.European Journal of Control,2011,17(5):568–578.

Biographies

Chao Wangwas born in 1982.He received his B.S.degree atSchoolof Mathematics from Nankai University.He is currently a Ph.D.candidate atthe School of Computer and Information Technology from Beijing Jiaotong University.His research interests are in the fields offormalmethods and symbolic computation.

E-mail:wangchao@bjtu.edu.cn.

Jinzhao Wuwas born in 1965.He received his Ph.D.degree in science from Institute of Systems Science,Chinese Academy of Sciences.He is now a professor in the College of Information Science and Engineering,GuangxiUniversity for Nationalities,a concurrent professor of Computer and Information Technology,Beijing Jiaotong University,and a researcher at Chengdu Institute of Computer Application,Chinese Academy of Sciences.His research interests are in the fields offormalmethods,symbolic computation,and automated reasoning.

E-mail:wujz2009@gmail.com.

Hongyan Tanwas born in 1966.She received her M.S.degree in computer science at Lanzhou University.She is now a research associate at the Institute of Acoustics,Chinese Academy of Sciences. Her research interests are in the fields of distributed computing systems and peer-to-peer systems.

E-mail:wcharles8@sina.com.

10.1109/JSEE.2015.00096

Manuscript received April 15,2014.

*Corresponding author.

This work was supported by the National Natural Science Foundation of China(11371003;11461006),the Natural Science Foundation of Guangxi(2011GXNSFA018154;2012GXNSFGA060003),the Science and Technology Foundation of Guangxi(10169-1),the Scientific Research Project from Guangxi Education Department(201012MS274), and Open Research Fund Program of Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis(HCIC201301).