当前位置：文档库 › Abstract On timed models and full abstraction

Abstract On timed models and full abstraction

On timed models and full abstraction

Gavin Lowe and Jo¨e l Ouaknine1

Oxford University Computing Laboratory

Wolfson Building,Parks Road

Oxford,OX13QD,UK.

Abstract

In this paper we study a denotational model for a discrete-time version of CSP. We give a compositional semantics for the language.The model records refusal information at the end of each time unit;we believe this model to be simpler than existing models.We also show that the model is fully abstract:equivalence in the model corresponds to the natural equivalence of may testing;and all members of the denotational model are syntactically expressible.We also consider a slightly weaker model,containing no refusal information;we show that this model corresponds to an alternative form of may testing.We brie?y discuss the application of these models to the study of information?ow in multi-level secure systems.

Key words:Process algebra,timed models,full abstraction,CSP.

1Introduction

In this paper,we consider denotational semantic models for a discrete-time version of CSP[2,10].In particular,we present a compositional model,the timed testing model,for the language,which is fully abstract with respect to may testing,and hence is the coarsest reasonable model of the language.The original model for the language,the refusal traces model2from[6],represented a process by the set of its refusal traces,where a refusal trace is an alternating sequence of sets of events that are refused,and events that are performed by the process.The model of this paper records fewer refusal sets:it records refusals only before the special event tock that represents the passage of one time unit.

Our interest in this model arises from our work on information?ow in multi-level secure systems.In a multi-level secure system,users are given se-1Email:gavin.lowe@https://www.wendangku.net/doc/707980120.html,,joel.ouaknine@https://www.wendangku.net/doc/707980120.html,

2The model was originally called the refusal testing model;we use the name refusal traces, because we will be using the word“testing”in a di?erent sense.

This is a preliminary version.The?nal version will be published in

Electronic Notes in Theoretical Computer Science

URL:www.elsevier.nl/locate/entcs

curity clearances(for example,“Top Secret”,“Secret”,“Con?dential”,“Un-classi?ed”).The question,then,is whether a user with a high classi?cation level can pass information to a user with a lower classi?cation level,and if so how much.In[4],we introduced a de?nition for the quantity of information that can be passed in such a system modelled in CSP.It turned out that the appropriate semantic model for this analysis was the timed testing model we consider in this paper.In that earlier paper,we de?ned that model as a projection of the refusal traces model from[6].The current paper consid-ers the timed testing model in more detail,and can be seen as building the foundations for the earlier paper.

Let’s look at an example.Suppose the system is willing to perform an event h from a high level user High,after which it will perform an event l of a low level user Low,and then return to its initial state after one time unit:

System=h→l→W ait1;System.

How can High exploit this to pass information to Low?One tactic would be to perform h whenever he wants to pass a1bit,and to do nothing when he wants to pass a0bit;if we model the choice of bit by an input on channel in, this tactic is captured by the following process:

High=in?x→if x=1then h→W ait1;High else W ait1;High. Low can then try to perform l;if this succeeds,then he knows High was trying to pass1;if this fails,he can timeout after one time unit and deduce that High was trying to pass0:

Low=(l→W ait1;out!1→Low)1￡(out!0→Low).

When we combine these processes in parallel,hiding the internal communica-tions:

((High

{h}System)

{l}

Low)\{h,l}

the resulting system acts as a reliable bu?er from in to out(albeit with a small delay).Hence this system can be used to pass one bit per time unit.

One can think of Low as a testing process,testing High

{h}

System in order to ascertain its behaviour.What is the appropriate model in which to reason about such systems?Clearly,we need some kind of refusal testing model[8,5] (i.e.where refusal information is recorded throughout a trace,rather than just at the end),for Low needs to be able to detect refusals of the system —corresponding to0bits in the example—and then continue testing.The inclusion of time in the model is necessary if we are to talk about?ows of information caused by timing,or about the rate of information?ow;it has the fortunate consequence of allowing observation of refusals to correspond to testing(as shown in Section6).However,it turns out that the only refusals Low can detect—and that should be included in the model—are those just before a tock event:such refusals can be detected by employing a timeout,as in the above example.

In[4]we de?ned such a model as a projection of the timed refusal traces model(the model in this paper is isomorphic to,but slightly simpler than, the model in that paper),but did not study its properties.In this paper,we give a compositional semantics to discrete time CSP within this model.We then show that the model is fully abstract:two processes are distinguished in the model if and only if they are distinguished by may testing;and the model contains no junk,i.e.every element of the semantic domain corresponds to a syntactically-de?nable process.

In Section2we review the syntax of discrete-time CSP,and in Section3 we describe the refusal traces model from[6].In Section4we de?ne the timed testing model,giving it a compositional semantics,and in Section5 we consider the relationship between the two models,presenting a projection from the former to the latter.In Section6we prove the full abstraction result. Finally,in Section7,we consider a model that records no refusal information: this model is not compositional,but can be de?ned as a projection of the timed testing model;we show that equivalence in this model corresponds to an alternative form of may testing.Some proofs are omitted because of lack of space;they can be found in the full version of the paper.

2Timed CSP syntax

LetΣbe a?nite set of events.We assume a special event tock(not inΣ)that represents the passage of one time unit.We de?neΣtock=Σ∪{tock}.

In the notation below,we have a∈Σand A?Σ.The parameter n ranges over the non-negative integers N.R represents a renaming relation R:Σ?Σ. The variable X is drawn from a?xed in?nite set of process variables V AR.

Timed CSP terms are constructed according to the following grammar: P:=ST OP|a→P|W ait n;P|P1n￡P2|P1P P2|P1 P2| P1

P2|P\A|P[R]|X|μX r P.

These terms have the following intuitive interpretations:

?ST OP is the deadlocked,stable process that is only capable of letting time pass.

?a→P initially o?ers to engage in the event a at any time,and subsequently behaves like P.

?W ait n;P is the process that idles for n time units,and then becomes P.

?P n

￡Q is a timeout process that initially o?ers to act like P for n time units,

after which it silently becomes Q if P has failed to communicate any visible event.

?P Q represents the nondeterministic(or internal)choice between P and Q;which of these two processes P Q becomes is independent of the environment:how the choice is resolved is considered to be outside the

domain of discourse.

?P P Q,on the other hand,denotes a process which is willing to behave either like P or Q,at the choice of the environment;this decision is taken on the?rst visible event that is communicated.

?P1

A P2is a parallel composition of P1and P2,synchronising on all events

in A.

?P\A is a process that behaves like P but with all communications in the set A hidden(made invisible to the environment);the assumption of maximal progress,orτ-urgency,dictates that no time can elapse while hidden events are on o?er—in other words,hidden events happen as soon as they become available.

?P[R]is a process that behaves like P except all the(non-tock)events are renamed according to the relation R;so if P can perform a,then P[R] can perform any b such that aRb;note that the renaming leaves tock s un-changed3.

?The process variable X has no intrinsic behaviour of its own,but can imitate any process P as part of a recursion—see below.

?The recursionμX r P represents a process which behaves like P but with every free occurrence of X in P(recursively)replaced byμX r P;semanti-cally,this corresponds to the unique solution to the equation X=P;note that the variable X here usually appears freely within P’s body.

Note our requirement that all delays(parameters n in the terms W ait n and P1n￡P2)be integral.This restriction is essentially harmless,because of the freedom to scale time units.We could equivalently have required rational delays,as many authors do.

Within the recursive processμX r P,we specify that X should be time-guarded in P,i.e.the process cannot recurse without any time passing.This condition prevents Zeno processes that do not allow time to progress.Su?-cient syntactical conditions for time-guardedness are given in[6].

We introduce some derived constructs.We write i:I P i and2i:I P i for indexed internal and external choices,respectively,indexed by the?nite set I. We write?a:A→P(a)for2a:A a→P(a),i.e.a process that initially o?ers the events of A,and when one of them is performed acts like the correspond-ing P(a).We write P|||Q for an interleaving of P and Q,i.e.P

{}

Q.We also tend to express recursions by means of the equational notation X=P, rather than the functionalμX r P prescribed by the de?nition.

We use the conventions that pre?xing(→)and sequential composition(;) bind tighter than the binary choice operators( ,P,￡).

3This construct generalises the functional renaming(f(P))and inverse renaming(f?1(P)) constructs found in early versions of CSP.

Note that we change the semantics of the timeout operator slightly from that of[6,7]:our timeouts are strict,in the sense that events of P cannot be performed by P n￡Q after the n th tock;by contrast,in[6,7],events of P are still available(unstably)after the n th,but before the n+1th,tock.This non-strict timeout,written as“n￡”,can be de?ned as a derived operator,as follows:

P n￡Q=(P P W ait n;trig→Q)\{trig},

where trig is a fresh event.(By contrast,the strict timeout cannot be de?ned as a derived operator.)We originally introduced the strict timeout because it seems more appropriate for modelling purposes:for example,it is necessary in the information?ow example from the introduction.Moreover,it also seems to be necessary for the“no junk”result in Section6.

3The timed refusal traces model

The timed refusal traces model,in common with most semantic models of CSP,contains information about both which events are performed,and which events are refused by the process.Recall that a set of events X is said to be refused by a process P if P is stable,i.e.is unable to perform any internal events,and is unable to perform any of the events from X.The timed refusal trace model for CSP records refusal information about a process throughout a trace(by contrast,the untimed stable failures model[10]records refusal information only at the end of the trace).

However,it might be the case that no refusal information can be recorded at a particular point in a trace,because the process does not enter a stable state.For example,consider the process(a→ST OP P b→ST OP)\{a}. If this process performs a b,then it does so from an unstable state,where the internal event a is available;hence no refusal can be observed before the b. The model deals with this situation by using a null refusal,written as?, to indicate that no refusal information was recorded,possibly because the process did not enter a stable state;for example,the above process has the trace ?,b,{a,b,c} .

Formally,we de?ne the set REF of refusal information by

REF =PΣ∪{?}.

We lift the normal set operators to REF in the obvious way(decorating the lifted versions with“?”),treating?as being below the empty set;for example, for x∈Σ,X∈PΣ,we have???X;?∪?X=?∩?X=?;?(x∈??).

The timed refusal trace model for CSP represents a process by its refusal traces,i.e.alternating sequences of the form X0,a1,X1,a2,...,a n,X n ,where each a i∈Σtock represents the performance of the event a i,and each X i∈REF represents refusal information.Formally,we de?ne refusal traces using the regular expression

RefusalTrace =REF.(Σtock.REF)?.

We de?ne some operations over refusal traces.trace(tr)removes all refusal information from tr:

trace( ) = ,

trace( a tr) = a trace(tr),if a∈Σtock,

trace( X tr) =trace(tr),if X∈REF.

refusals(tr)returns the set of events that are refused during tr4: refusals(tr) = {X∈PΣ|X in tr}.

tr tr indicates that tr contains less information than tr in the sense that tr is a pre?x of tr ,or it contains smaller refusal sets,or a combination of the two.Formally, is the smallest relation satisfying

X Y tr?X??Y,

X,a tr Y,a tr ?X??Y∧tr tr .

The refusal traces model M R contains those S?RefusalTrace such that the following conditions hold,where a ranges overΣand A over REF5.

R1. ? ∈S;

R2.tr∈S∧tr tr?tr ∈S;

R3.tr ?,tock tr ∈S?tr {},tock tr ∈S;

R4.A=?∧tr A tr ∈S∧tr A,a,? /∈S?tr A∪{a} tr ∈S;

R5.tr∈S?tr tock,? ∈S;

R6.tr A,a tr ∈S?a/∈?A;

R7.?k∈N r?n∈N r?tr∈S r#(tr`|tock)≤k?#(trace(tr))≤n. The?rst condition says that the minimal behaviour ? can always be ob-served.The second condition says that the observations of S are downwards-closed.Condition R3says that a process will stabilise before a tock,so at least the empty set can be refused.Condition R4says that if a process can stably refuse A,and cannot perform a,then a can be added to the refusal set. Condition R5says that time cannot be stopped.Condition R6says that an event a cannot be refused and then performed.Condition R7is a bounded-speed condition:there is a bound n on the number of events that can be performed in the?rst k time units.6

4The notation x in tr indicates that x is an element of the sequence,or trace,tr.

5The operator`|restricts a trace to a particular event or set of events.

6In[6],there was an extra condition:A=?∧tr A,a,? ∈S?tr A,tock,?,a,? ∈S, which says that if an event is stably available,then it will still be available after a tock. This condition is not satis?ed by our strict timeout operator.Further,it seems less natural to us than the other conditions.

3.1Semantic de?nitions

We can de?ne a semantic function

R :CSP →(V AR →M R )→M R ,such that R [[P ]]ρgives the refusal traces of P ,assuming environment ρgives the semantics for free variables of P .Throughout the following de?nitions,tr ranges over RefusalTrace ,and tr

over pre?xes of elements of RefusalTrace ending in an event.

R [[ST OP ]]ρ ={tr |trace (tr )∈tock ?},

R [[a →P ]]ρ

={tr |trace (tr )∈tock ?∧a /∈refusals (tr )}∪

{tr a tr |trace (tr )∈tock ?∧a /∈refusals (tr )∧tr ∈R [[P ]]ρ},

R [[W ait n ;P ]]ρ

={tr |trace (tr )

{ tr

tr |trace ( tr )=tock n ∧tr ∈R [[P ]]ρ},R [[P P Q ]]ρ

={tr |trace (tr )∈tock ?∧tr ∈R [[P ]]ρ∩R [[Q ]]ρ}∪

{tr a tr |trace (tr )∈tock ?∧tr ∈R [[P ]]ρ∩R [[Q ]]ρ∧

a ∈Σ∧tr a tr ∈R [[P ]]ρ∪R [[Q ]]ρ},

R [[P Q ]]ρ =R [[P ]]ρ∪R [[Q ]]ρ,

R [[P n ￡Q ]]ρ

={tr |tr ∈R [[P ]]ρ∧tock n ≤trace (tr )}∪

{ tr

tr | tr ? ∈R [[P ]]ρ∧trace ( tr )=tock n ∧tr ∈R [[Q ]]ρ},R [[P A Q ]]ρ ={tr |?tr P ∈R [[P ]]ρ,tr Q ∈R [[Q ]]ρr tr ∈tr P A tr Q },

R [[P \A ]]ρ =RefCl {tr \A |tr ∈R [[P ]]ρ∧tr is A -urgent },

R [[P [R ]]]ρ ={tr |?tr ∈R [[P ]]ρr tr R ?tr },

R [[X ]]ρ =ρ(X ),

R [[μX r P ]]ρ =the unique ?xed point of the mapping C :M R →M R

given by C (S ) =R [[P ]]ρ[S/X ].

The semantics of parallel composition,hiding and renaming use some aux-iliary functions.tr P A

tr Q represents the set of traces that can be formed from the parallel composition of traces tr P and tr Q ,synchronising on events from A tock =A ∪{tock };this operator is de?ned by the equations in Figure 1and the obvious symmetric equations.Within that de?nition,if the two pro-cesses refuse X and Y respectively,then the composition can refuse any set from

X ∩A Y ={C |C ??(X ∩?A )∪?(Y ∩?A )∪?(X ∩?Y )}.7

A Y ={ C |C∈X∩

Y},

X,x tr

Y =

if x∈A tock then{}else{ C,x tr |C∈X∩

A Y∧tr ∈tr

Y },

X,x tr

Y,y tr = if x/∈A tock∧y∈A tock then{ C,x tr |C∈X∩

A Y∧tr ∈tr

Y,y tr }

else if x∈A tock∧y/∈A tock

then{ C,y tr |C∈X∩

A Y∧tr ∈ X,x tr

tr }

else if x/∈A tock∧y/∈A tock

then{ C,x tr |C∈X∩

A Y∧tr ∈tr

Y,y tr }∪

{ C,y tr |C∈X∩

A Y∧tr ∈ X,x tr

tr }

else if x=y∈A tock

then{ C,x tr |C∈X∩

A Y∧tr ∈tr

tr }else{}.

Fig.1.Parallel composition of traces in the refusal traces model

tr is A-urgent?

?X∈REF;tr ,tr |tr=tr X,tock tr r A??X.

X \A =if A??X then X else ? ,

( X,x tr)\A =if x∈A then tr\A else( X \A) x (tr\A).

RefCl S ={tr|?tr ∈S r tr tr }.

X R Y?X=Y=?∨X={x|?y∈Y r xRy}.

X R? Y ?X R Y,

( X,tock tr)R?( Y,tock tr )?X R Y∧tr R?tr , ( X,x tr)R?( Y,y tr )?X R Y∧xRy∧tr R?tr ,for x,y∈Σ.

Fig.2.Auxiliary semantic de?nitions for hiding and renaming Auxiliary semantic de?nitions relating to the de?nitions for P\A and P[R]are in Figure2.The assumption about the urgency of hidden events is captured by the fact that we consider only A-urgent traces of P:traces where all of A can be refused before a tock.tr\A represents the e?ect of hiding A in tr.RefCl S forms the downwards closure of S.For example,if

P=a→(b→ST OP P a→ST OP),

then P\{a}has the refusal trace ?,b,{b},tock,? ,corresponding to the refusal trace {b},a,{c},b,{a,b},tock,? (among others)of P;note that{a}-urgency is necessary to ensure that a tock cannot happen before the?rst a or

the b. R represents the lifting of the renaming relation R to REF,and R?represents the lifting to refusal traces.

In[6]it is shown that this denotational semantics is congruent to the operational semantics.The following theorem is adapted from[6]. Theorem3.1The mapping R is well de?ned.

4The timed testing model

In this section we present the timed testing model for discrete-time CSP. The model records refusal information only before tock s.Further,we can do away with the null refusals?(essentially because of condition R3)and only record actual refusals from PΣ.Timed tests can be de?ned using the following regular expression.

TimedTest =(Σ+PΣ.tock)?.

Note that refusals are recorded before,and only before,tock s;for example a,b,{b,c},tock,{},tock,c .

Note that this model fails to distinguish processes that are distinguished in the refusal traces model.For example,consider:

P =((a→ST OP1￡ST OP) ST OP),

Q =(a→ST OP P b→ST OP)\{b}.

These are distinguished in the refusal traces model,for P has the refusal trace {},a,? ,which Q does not,for Q performs a from an unstable state. However,P and Q are equivalent in this model,for they can both perform an a only before the?rst tock,and can refuse anything before a tock.In Section5we show that the refusal traces model distinguishes all processes that are distinguished by this model,so this model is strictly more abstract.

We adapt some operations from refusal traces to timed tests.trace(tr) removes all refusal information from tr.refusals(tr)gives the set of all events that are refused anywhere in tr.These two operations are de?ned analogously to as in the refusal trace model.tr tr indicates that tr contains less information than tr :

tr,

a tr a tr ?tr tr ,

X,tock tr Y,tock tr ?X?Y∧tr tr .

The timed testing model M T contains those S?T imedT est such that the following conditions hold:

T1. ∈S;

T2.tr∈S∧tr tr?tr ∈S;

T3.tr A,tock tr ∈S∧tr a /∈S?tr A∪{a},tock tr ∈S;

T4.tr∈S?tr {},tock ∈S;

T5.?k∈N r?n∈N r?tr∈S r#(tr`|tock)≤k?#(trace(tr))≤n. These conditions correspond closely to conditions R1,R2,R4,R5and R7, respectively.

4.1Semantic de?nitions

We can de?ne a semantic function

T:CSP→(V AR→M T)→M T,

such that T[[P]]ρgives the timed tests of P,assuming environmentρgives the semantics for free variables of P.Throughout these equations,tr ranges over TimedTest.

T[[ST OP]]ρ ={tr|trace(tr)∈tock?},

T[[a→P]]ρ =

{tr|trace(tr)∈tock?∧a/∈refusals(tr)}∪

{tr a tr |trace(tr)∈tock?∧a/∈refusals(tr)∧tr ∈T[[P]]ρ}, T[[W ait n;P]]ρ =

{tr|trace(tr)

{tr tr |trace(tr)=tock n∧tr ∈T[[P]]ρ},

T[[P P Q]]ρ =

{tr|trace(tr)∈tock?∧tr∈T[[P]]ρ∩T[[Q]]ρ}∪

{tr a tr |trace(tr)∈tock?∧tr∈T[[P]]ρ∩T[[Q]]ρ∧

a∈Σ∧tr a tr ∈T[[P]]ρ∪T[[Q]]ρ},

T[[P Q]]ρ =T[[P]]ρ∪T[[Q]]ρ,

T[[P n￡Q]]ρ =

{tr|tr∈T[[P]]ρ∧tock n≤trace(tr)}∪

{tr tr |tr∈T[[P]]ρ∧trace(tr)=tock n∧tr ∈T[[Q]]ρ},

T[[P

A Q]]ρ ={tr|?tr P∈T[[P]]ρ,tr Q∈T[[Q]]ρr tr∈tr P

tr Q},

T[[P\A]]ρ =RefCl{tr\A|tr∈T[[P]]ρ∧tr is A-urgent},

T[[P[R]]]ρ ={tr |?tr∈T[[P]]ρr tr R?tr },

T[[X]]ρ =ρ(X),

T[[μX r P]]ρ =the unique?xed point of the mapping C:M T→M T

given by C(S) =T[[P]]ρ[S/X].

The auxilliary operators relating to parallel composition,hiding and re-naming are similar to as in Figures1and2.

Theorem4.1The mapping T is well de?ned.

Proof.We need to show that ifρ∈V AR→M T then T[[P]]ρ∈M T,i.e.that T[[P]]ρsatis?es the healthiness conditions of the semantic model.This is a

large structural induction;most cases are straightforward.As an illustrative

example,we include the proof of T4for hiding.

Suppose tr∈T[[P\A]]ρ.Then there is some tr ∈T[[P]]ρsuch that tr is

A-urgent,and tr∈RefCl{tr \A}.We show that,after tr ,for every n,either

n events from A can be performed,or all of A can be refused after k

events:

?n∈N r?a1,...,a n∈A r tr a1,...,a n ∈T[[P]]ρ∨

case,suppose tr a1,...,a n ∈T[[P]]ρ.If there is some a n+1∈A such that

tr a1,...,a n+1 ∈T[[P]]ρthen we are done.Otherwise,by T4we have that

tr a1,...,a n,{},tock ∈T[[P]]ρ.Then by repeated use of T3we have that

tr a1,...,a n,A,tock ∈T[[P]]ρ,as required.

Because of condition T5,there is a bound on the number of events that

can be added to the trace using the process in the previous paragraph.Hence

we have that tr =tr a1,...,a k,A,tock ∈T[[P]]ρfor some a1,...,a k∈A. Now,tr is A-urgent,and tr {},tock ∈RefCl{tr \A}so tr {},tock ∈

T[[P\A]]ρ,as required.

The case of recursion is almost identical to as in[6]for the refusal testing

model.An ultra metric is de?ned over M T as follows.Given S∈M T,write

S(t)for those refusal traces in S containing fewer than t tocks: S(t) ={tr∈S|#(trace(tr)`|tock)

(In particular,S(0)={}.)Informally,if two processes behave the same

before time t,but then behave di?erently,then they are at distance2?t;more

precisely:

d(S,S ) =inf{2?t|S(t)=S (t)}.

One can then show that M T is a complete metric space with respect to

this metric.If P is time-guarded in X,then the corresponding mapping

C(S) =T[[P]]ρ[S/X]is a contraction mapping,i.e.:

d(C(S),C(S ))≤1

d(S,S ).

One can then use Banach’s?xed point theorem(see e.g.[13])to show that C has a unique?xed point,and further that?xed point equals lim n→∞C n(Q) for an arbitrary process Q.P Note that the existence of a compositional semantic function implies that equivalence in this model is a congruence with respect to the CSP operators.

5Relating the two models

In this section we consider the relationship between the refusal trace and timed testing models.Recall that there are two di?erences between the two models:

(1)the timed testing model contains refusal information only before tock s; and(2)the timed testing model does not use the null refusal?.We therefore de?ne a function

f:RefusalTrace→TimedTest

that maps a refusal trace by the corresponding timed test by(1)removing all refusal information except that preceding tock s;and(2)replacing any occurrence of?before tock by{}:

f( A ) = ,

f( A,a tr) = a f(tr),for a∈Σ,

f( ?,tock tr) = {},tock f(tr),

f( A,tock tr) = A,tock f(tr),for A∈PΣ.

We then lift f to sets of refusal traces by pointwise application: f(S) ={f(tr)|tr∈S}.

We begin by showing that f maps elements of M R into M T:

Theorem5.1If S∈M R then f(S)∈M T.

Proof.(sketch)That f(S)satis?es the axioms of M T can be easily shown from the fact that S satis?es the corresponding axioms of M R.P We now show that f maps any syntactic process in M R to the corre-sponding process in M T,i.e.f forms a homomorphism with respect to the CSP operators.

Theorem5.2If?X rρT(X)=f(ρR(X))then T[[P]]ρT=f(R[[P]]ρR). Proof.(sketch).This is a large structural induction over the syntax of the language.Some cases can be simpli?ed as follows.De?ne the function

g:TimedTest→RefusalTrace

to insert?before every element ofΣand at the end of the trace:

g( ) = ? ,

g( a tr) = ?,a g(tr),for a∈Σ,

g( A,tock tr) = A,tock g(tr).

Note that f(g(tr))=tr.Then the result of the theorem is equivalent to the following two statements:

?tr∈RefusalTrace r tr∈R[[P]]ρR?f(tr)∈T[[P]]ρT,

?tr∈TimedTest r tr∈T[[P]]ρT?g(tr)∈R[[P]]ρR.

Proving these two statements,inductively,is straightforward in most cases.

For recursion,consider the recursive processμX r P.Let C T:M T→M T and C R:M R→M R be the corresponding mappings on the seman-tic models,i.e.C T(S) =T[[P]]ρT[S/X],and C R(S) =R[[P]]ρR[S/X].Our structural induction hypothesis shows that

C T(f(S))=T[[P]]ρT[f(S)/X]=f(R[[P]]ρR[S/X])=f(C R(S)).

As shown in the?xed point theorems,the?xed points are the limits of the sequences(R n)n∈N and(T n)n∈N,where

T0 =T[[ST OP]]ρT,T n+1 =C T(T n),

R0 =R[[ST OP]]ρR,R n+1 =C R(R n).

We show that T n=f(R n)by induction on n.The base case is trivial.For the inductive case:

T n+1=C T(T n)=C T(f(R n))=f(C R(R n))=f(R n+1),

using the inductive hypothesis and the above result.Hence

T[[μX r P]]ρT=lim n→∞T n=lim n→∞f(R n)

=f(lim n→∞R n)=f(R[[μX r P]]ρR),

using the continuity of f.P 6Full abstraction

A semantic model is said to be fully abstract if the following two conditions hold[10]:

?Whenever two processes P and Q are distinguished by the semantics,then they are distinguished by some natural criterion:typically this criterion is the existence of a context C[]such that one of C[P]and C[Q]passes,and the other fails,some simple test.

?Every element of the semantic model corresponds to a syntactically ex-pressible process(taking a liberal view of expressibility,for example allowing mutual recursions to be indexed by non-constructive mathematical objects); this condition is sometimes referred to as“no junk”.

(The no junk condition is not always considered to be part of full abstraction.) In the next subsection we prove that the timed testing model satis?es the former condition by showing that equivalence in the model corresponds to may testing equivalence[1].In the following subsection we show that the model satis?es the no junk condition.

6.1Timed may testing

A timed test process is simply a timed CSP process that can perform a spe-cial eventω/∈Σrepresenting success.When de?ning test processes,it is convenient to use the following de?nitions:

SUCCEED =ω→ST OP,FAIL =ST OP.

We say that P may pass the test T,written P may T,if the parallel composition of P and T,hiding all events fromΣ,can performω: P may T =?tr∈T[[(P

T)\Σ]]rωin tr.

Note that the e?ect of hidingΣis to make all these events urgent,correspond-ing to the intuition that if both P and T can do an event,then it happens immediately.Note also that the above de?nition could have used the semantic function R instead of T:both models agree on the performance of events.

We say that two processes P and Q are timed testing equivalent if they pass precisely the same tests:

P≡may Q =(?T∈T est r P may T?Q may T).

We now prove that timed testing equivalence indeed corresponds to equiva-lence in the timed testing model.

Theorem6.1P≡may Q?T[[P]]=T[[Q]].

Proof.For the right-to-left direction note that if T[[P]]=T[[Q]]then for all

tests T,T[[(P

ΣT)\Σ]]=T[[(Q

T)\Σ]],using the compositional semantics

we gave earlier;hence P may T?Q may T.

For the left to right direction,we prove the contrapositive.Suppose T[[P]]=T[[Q]].Then without loss of generality,there is some tr∈T[[P]] such that tr/∈T[[Q]].Let

tr= a11,a12,...,a1m

,A1,tock,

a21,a22,...,a2m

,A2,tock,

...

a n1,a n2,...,a nm n .

For convenience,we de?ne a syntactic operator that attempts an event for one time unit,failing if it is not accepted:

a?→T =(a→T)1￡FAIL.

We construct a test that succeeds when the process it is testing performs the trace tr,but fails,otherwise:

T =a11?→a12?→...?→a1m

1?→(?x:A

→FAIL

￡a21?→a22?→...?→a2m

2?→(?x:A

→FAIL

￡...

￡a n1?→a n2?→...?→a nm n?→SUCCEED)...).

Note that the only way that T can reach the SUCCEED state is if the process it is testing can perform the trace tr:clearly the processes need to perform the a ij and tock events in the appropriate order;and if the tested process can perform some x from A i at the appropriate point,then that event will be performed(because it is hidden in the testing system),and so T will enter a FAIL state;the only way the tested process can prevent this from happening is by refusing all of A i.Hence P may T but not Q may T.P In untimed models,may-equivalence is the same as traces equivalence[1], i.e.with no refusal information;in continuous-time models,may-equivalence

is the same as?nite failures equivalence[11],i.e.with full refusal information; an interesting consequence of the above theorem is that may-equivalence in the discrete-time model lies between the may-equivalences in these other two scenarios.

6.2No junk

In this section we show that every element of the semantic model M T is de?nable using the CSP syntax;i.e.the model contains no junk.

For S∈M T,de?ne the initial events,the initial maximum refusals of S, and the behaviours of S after event a and after A,tock as follows:

inits(S) ={a| a ∈S},

initMaxRefs(S) ={A| A,tock ∈S∧A?Σ?inits(S)},

S after a ={tr| a tr∈S},

S after A,tock ={tr| A,tock tr∈S}.

Note that for S∈M T:

?if a∈inits(S)then S after a∈M T;

?if A∈initMaxRefs(S)then S after A,tock ∈M T;

?if B,tock ∈S then B∪(Σ?inits(S)),tock ∈S by repeated use of T3, and so B∪(Σ?inits(S))∈initMaxRefs(S);

?initMaxRefs(S)containsΣ?inits(S):this follows from the previous item because {},tock ∈S by T1and T4.

Given S∈M T,we now de?ne a process P(S)that has precisely the behaviours in S:

P(S) = A:initMaxRefs(S) ?x:Σ?A→P(S after x)

￡P(S after A,tock ). (We note that P(S)may not be?nitely expressible,because of the indexing by potentially non-constructive sets;we are not considering e?ective computabil-ity here.)

Lemma6.2?S∈M T r T[[P(S)]]=S.

Proof.We begin by showing that for every timed test tr,for every S∈M T, if tr∈S then tr∈T[[P(S)]].The proof is by induction on the length of tr. The base case is trivial.So suppose tr∈S is non-empty,and perform a case analysis as follows:

?Case tr= a tr .Then a∈inits(S)and tr ∈S after a;so by the inductive hypothesis,tr ∈T[[P(S after a)]].Hence,letting A =Σ?inits(S),we have a∈Σ?A and so tr∈T[[?x:Σ?A→P(S after x)]], and so tr∈T[[P(S)]]because A∈initMaxRefs(S).

?Case tr= B,tock tr .Let A =B∪(Σ?inits(S)).Now,by repeated use of T3, A,tock tr ∈S,so A∈initMaxRefs(S).Hence tr ∈S after

A,tock ,and so by the inductive hypothesis tr ∈T[[P(S after A,tock )]]. Hence tr∈T[[?x:Σ?A→P(S after x)1￡P(S after A,tock )]]and so tr∈T[[P(S)]].

We now show the converse:that if tr∈T[[P(S)]]then tr∈S,for every S∈M T.The proof is by induction on the length of tr.The base case is again trivial.So suppose tr∈T[[P(S)]]is non-empty,and perform a case analysis over the form of tr:

?Case tr= a tr .Then for some A∈initMaxRefs(S),a∈Σ?A(so a∈inits(S)),and tr ∈T[[P(S after a)]].So by the inductive hypothesis, tr ∈S after a so tr∈S.

?Case tr= B,tock tr .Then for some A∈initMaxRefs(S),we have B?A and tr ∈T[[P(S after A,tock )]].Hence by the inductive hy-pothesis,tr ∈S after A,tock ,and so A,tock tr ∈S.But then tr= B,tock tr ∈S,because S satis?es T2.

Finally,we consider the time-guardedness of the P(S)recursions.The de?nition as it is written is not obviously time-guarded:however,we can transform it into a form where it is.Replace each recursive call of the form P(S after x)by the right-hand-side of the corresponding process de?nition; keep repeating this replacement.Now,S satis?es T5,so there is some up-per bound n on the number of events that can be performed before the?rst tock;hence the above replacement can be repeated at most n times before all branches meet processes P(S )with inits(S )={}.Then all recursive calls are on the right-hand-side of a timeout,so the de?nition of P(S)is time guarded in all variables.P Hence the semantic model M T satis?es the no junk condition: Theorem6.3For every S∈M T,there is a process P such that T[[P]]=S.

6.3Full abstraction

The results of this section may be summarised in the following result. Corollary6.4The timed testing model is fully abstract with respect to the test“can performω”.

7Traces

In this section,we consider a yet more abstract model for discrete-time CSP, namely a pure traces model,containing no refusal information.The semantics of a process can be de?ned by projecting from the timed tests: T r[[P]]={trace(tr)|tr∈T[[P]]}.

(Of course,the traces could also have been obtained by projecting from the refusal traces.)We will say that two processes are trace equivalent if they have

the same traces.

Our main reason for considering this model is that we want to make a connection between our de?nition of the quantity of information?ow from[4], and Shannon information?ow theory[12].In the latter,one considers a prob-abilistically unreliable channel,say between A and B.Further,the channel is generative[14]:it is always willing to output a single value to B(that value depending probabilistically on what was input by A).This means that B receives no extra information by seeing refusals:if the channel is willing to output y,then he gains the same information by seeing the rest of his al-phabet refused as by performing y itself.For this reason,it seems that B’s observational power in this setting corresponds to the traces model.

It is well known that this model is not a congruence.For example,let P=a→(b→ST OP1￡ST OP),P =P W ait2;P. Then T r[[P]]=T r[[P ]]:both are given by the regular expression tock?+ tock?.a.tock?+tock?.a.b.tock?.But T r[[P\{a}]]=T r[[P \{a}]]:the latter includes tock,tock,b ,whereas in the former process the a will be performed (silently)before the?rst tock,and so the b can only be performed before the ?rst tock.However,this model is a congruence with respect to all operators other than hiding.

7.1Testing

We now de?ne an alternative notion of timed may testing.Note that in the untimed setting,the standard de?nition of P may T:

ω ∈traces((P

T)\Σ)

is equivalent to

T)rωin tr.

?tr∈traces(P

When one lifts these two de?nitions to a timed setting,they turn out to be di?erent:the former corresponds to the de?nition from Section6;the latter corresponds to the de?nition below.

We write P may T if test T,in parallel with P—without hiding—can perform the eventω:

P may T??tr∈T[[P

T]]rωin tr.

We then say that P and Q are may equivalent if they pass the same tests: P≡may Q??T∈T est r P may T?Q may T.

Note this is di?erent from the de?nition of may.Consider

P=a→ST OP,T=(a→FAIL)1￡SUCCEED.

Then P may T(on trace {},tock,ω ),but not P may T(since the hiding ensures that the a happens before time1).By contrast,de?ne

Q=a→ST OP ST OP.

Then Q may T and Q may T.So may testing distinguishes P and Q;however, the above test does not distinguish P and Q under may testing,and,in fact, no other does,as con?rmed by the following theorem.

Theorem7.1P≡may Q?T r[[P]]=T r[[Q]].

Proof.For the left to right implication,we prove the contrapositive.Suppose P and Q do not have the same traces.Then without loss of generality,suppose

tr= a11,a12,...,a1m

,tock,

a21,a22,...,a2m

,tock,

...

a n1,a n2,...,a nm n

is a trace of P but not of Q.We construct a test that succeeds when the process it is testing performs the trace tr,but fails,otherwise:

T =a11?→a12?→...?→a1m

?→W ait1;

a21?→a22?→...?→a2m

?→W ait1;

...

a n1?→a n2?→...?→a nm n?→SUCCEED.

For the reverse direction,it is easy to show that

T r[[P

A T]]={tr|?tr P∈T r[[P]],tr T∈T r[[T]]r tr∈tr P

tr T},

where the parallel composition of traces is similar to as de?ned in Figure1.

Hence if T r[[P]]=T r[[Q]],then T r[[P

ΣT]]=T r[[Q

T]],so P may T?

Q may T.P 8Conclusions

In this paper we have studied a compositional denotational model for Timed CSP,which we consider to be simpler than existing models.Further,we have shown that equivalence in the model corresponds to timed may testing, and hence this is the coarsest reasonable model of the language.Further, we have shown that the model contains no junk,and so precisely captures the properties of expressible processes.Finally,we have considered a weaker model based on traces.

In this section,we brie?y discuss some consequences of our decision to introduce a strict timeout operator to the language;we then discuss some related and future work.

8.1On strict timeouts

As noted earlier,the strict timeout operator seems to have a far more natural semantics than the weak timeout;in particular,is seems necessary to model

some natural examples,such as the example from Section1.

The correspondence with timed may testing does not depend on the strict timeout.The construction in Section6.1can be adapted to work with a weak timeout,by replacing the de?nition of a?→T by

a?→T =(a→T)0￡F AIL,

i.e.the a is available initially,but will be withdrawn sometime before the?rst tock.The reader may check that the rest of the proof goes through as before.

However,without the strict timeout,the model of this paper does not satisfy the no junk condition.It can be shown that,without this strict timeout, all processes satisfy the condition

tr A,tock ∈S∧tr A∪{a},tock /∈S?tr A,tock,a ∈S, (1)

which says that if an event is not refused before a tock(so must be available), then it will still be available after a tock.Therefore,any semantic object that does not satisfy the above condition cannot be expressed syntactically without the strict timeout.

It is interesting to ask whether adding the above condition(1)as an ax-iom7,and still omitting the strict timeout,gives us no junk.We believe not. Consider the process that initially o?ers an a,and if that a is performed after n tock s then o?ers a b after a further n tock s.This can be modelled using the strict timeout by

P(0),where P(n)=(a→W ait n;b→ST OP)1￡P(n+1).

This process satis?es the extra axiom.However,we believe that it is not expressible without the strict timeout,for one cannot detect the precise time at which the a occurs.

In[6,7],it is shown that the discrete-time models satisfy a very close rela-tionship with the continuous-time models of Timed CSP from[9].It would be interesting to consider whether the continuous-time models can be extended with a strict timeout,and whether the same relationship would then hold with the model of this paper.

8.2Related work

In[3],a fully abstract denotational semantics is presented for an OCCAM-like language.The authors prove that processes distinguished by the denotational model are also distinguished by a criterion extracted from the operational semantics;we consider this a less natural criterion than may testing.(They do not consider the absence of junk.)Like us,they consider failures(actually convex closure of ready sets,which is equivalent).They consider a language with synchronous computation,and thus do not consider the relative order of events within the same time unit:hence the question of refusals between 7This condition is similar to the axiom from[6]discussed in footnote6.

non-tock events—the di?erence between the refusal traces and timed testing models—does not arise.

In[7],a di?erent kind of full abstraction result is proven.It is shown that if two processes are distinguished by the model,then there is a natural (i.e.,closed under inverse digitisation)speci?cationφ,such that one process satis?esφand the other doesn’t.

8.3Future work

As noted above,our main reason for considering the model of this paper was our interest in quantifying information?ow in multi-level secure systems.We want to continue this work.In particular,as noted in Section7,we want to relate our de?nition to Shannon information?ow,either using the timed testing model or the traces model.Further,we want to consider algorithms for calculating the quantity of information?ow of a given process,and,indeed, whether the problem is decidable in general.

Acknowledgements

We would like to thank Irek Ulidowski and the anonymous referees for useful comments about this work.

References

[1]R.de Nicola and M.C.B.Hennessy.Testing equivalences for processes.

Theoretical Computer Science,34:83–133,1984.

[2]https://www.wendangku.net/doc/707980120.html,municating Sequential Processes.Prentice Hall,1985.

[3]C.Huizing,R.Gerth,and W.P.de Roever.Full abstraction of a real-time

denotational semantics for an occam-like language.In Proceedings of the14th ACM Symposium on Principles of Programming Languages,pages223–236, 1987.

[4]G.Lowe.De?ning information?ow quantity.Journal of Computer Security,

12(3,4):619–653,2004.

[5]A.Mukarram.A Refusal Testing Model for CSP.D.Phil thesis,Oxford,1993.

[6]J.Ouaknine.Discrete Analysis of Continuous Behaviour in Real-Time

Concurrent Systems.D.Phil thesis,Oxford University,2000.

[7]J.Ouaknine.Digitisation and full abstraction for dense-time model checking.

In Proceedings of TACAS,2002.

[8]I.Phillips.Refusal testing.Theoretical Computer Science,1987.

[9]G.M.Reed and A.W.Roscoe.The timed failures-stability model for CSP.

Theoretical Computer Science,211:85–127,1999.

[10]A.W.Roscoe.The Theory and Practice of Concurrency.Prentice Hall,1997.

[11]S.Schneider.Concurrent and Real-time Systems:The CSP Approach.Wiley,

1999.

[12]C.E.Shannon and W.Weaver.The Mathematical Theory of Communication.

University of Illinois Press,1963.