On the expressive power of CSP refinement
Contents
1. THEOREM 2 2 The closed sets in N are precisely the inverse images of C under uniformly continuous CSP representable functions That all such inverse images are closed follows by a standard topological argument This type of analysis does not give us much practical help in designing reasonable ways of expressing predicates for FDR but it does suggest that most reasonable predicates can be expressed More than anything else the calculations above resemble those for a full abstraction result ordinary ones for CSP being in Ros98 and it is indeed a result in the same spirit To be of practical use a predicate would need F P and G P to be finite state if P is as well as each having finite syntax and the above certainly do not achieve this This is inevitable given the generality of the above result since the set of closed predicates is uncountable and the set of finitary F G is countable This is because the number of finite pieces of CSP syntax is countable In practical terms one will want to keep more careful control over the relationships between the traces being considered both for different failures of the predicate and between the different copies of P that are running we really do not want to start up several copies of P running to test every single potential failure of the predicate We now illustrate some techniques that can be used to do it more efficiently by means of an example This is deliberately chosen so it has2. Muk93 Mukkaram A A refusal testing model for CSP Oxford University D Phil thesis 1993 Phi87 Phillips I Refusal testing Theoretical Computer Science 50 pp241 284 1987 RSR04 Reed J N Sinclair J and Roscoe A W Responsiveness of inter operating components Formal Aspects of Computing 16 4 pp294 411 2004 Ros91 Roscoe A W Topology computer science and the mathematics of convergence in Topology and category theory in computer science Reed Roscoe and Wachter eds Oxford University Press 1991 Ros92 Roscoe A W An alternative order for the failures model Journal of Logic and Computation 2 5 pp557 577 1992 Ros93 Roscoe A W Unbounded nondeterminism in CSP Journal of Logic and Computation 3 pp131 172 1993 Ros95 Roscoe A W CSP and determinism in security modelling Proceedings of 1995 IEEE Symposium on Security and Privacy IEEE Computer Society Press 1995 Ros98 Roscoe A W The theory and practice of concurrency Prentice Hall International 1998 This reference contains almost all necessary background on CSP It like the rest of the author s papers listed here other than Ros03 can be viewed or down loaded via http web comlab ox ac uk oucl work bill roscoe pubs html Ros03 Roscoe A W On the expressiveness of CSP refinement checking Draft version Proceedings of AVoCS 03 Southampton University Technical Report Ros04 Roscoe A W Finitary refinement checks for infinitary s
3. inf 2 P n Q n failures divergences refinement reverse containment traces refinement refinement over U Models T traces model N failures divergences model divergence strict N divergence and free portion of M F stable failures model u failures divergences infinite traces model divergence strict im On the expressive power of CSP refinement 21 Acknowledgements I would like to thank Joy Reed and Jane Sinclair for inspiring this work via their client server predicates and Ranko Lazi for his earlier work on determinism Michael Goldsmith Joel Ouaknine Gavin Lowe and Christie Bolton provided helpful comments on earlier drafts The clarity of the paper was greatly improved by comments from anonymous referees The work reported here was funded by grants from ONR and EPSRC References FDR Formal Systems Europe Ltd Fatlures Divergence Refinement User Manual obtainable from http www formal demon co uk fdr2manual index html Hoa85 Hoare C A R Communicating sequential processes Prentice Hall 1985 Laz98 Lazi R S A semantic study of data independence with applications to the mechanical verification of concurrent systems Oxford University D Phil thesis 1998 LMCO01 Leuschel A Massart T and Currie T How to make FDR Spin LTL model checking of CSP using refinement In Oliviera J N and Zave P Eds Proceedings of Formal Methods Europe FME 2001 LNCS 2021 DSSE TR 2000 10 pages 99 118
4. Namely G U f f E U Consider Q 1 Qr T G Note that all such I are proper subsets of by our assumption that gt 1 Since R is distributive we have R Q and by construction e Y C failures Q as this is true for each individual Qr and e N failures Q Y since for each s X Y there is T G with s X Er It follows by the fact that Y are assumed to refute R that we have a contradiction to the assumption that Y gt 1 We therefore need only consider the cases of Y where Y is empty or a singleton set If Y is empty it means that for failures P to contain no member of the corresponding implies R P On the other hand if Y s X then it means that if R P holds and s X failures P then failures P must contain at least one member of Y We can actually guarantee that each occurs in our Refr with its minimised elements only with Y 0 or only with singletons For if f Refr then clearly f refutes R and is less than both Whether f were there or not R would be refuted by one or the other It is easy to see that any R represented by such a Ref is distributive for if P N Q were refuted by some 0 then it is clear both P and Q are neither can contain any member of And if it were refuted by f then as nondeterministic choice is union one of P and Q must contain the failure f and neit
5. Appendix A of Ros98 contains a tutorial on metric spaces from the CSP perspective In fact the properties specifically topological compactness of M with finite mean uniform continuity is equivalent to ordinary metric continuity where 6 is allowed to vary with z as well as with e DEFINITION 2 2 A predicate R is said to be closed if the set P R P is closed in the metric topology So suppose F and G are both UC CSP contexts which cannot introduce divergence This is equivalent to F Chaosy and G Chaosy being divergence free Since any failure of the refinement f shows up in some finite length behaviours i e if H nE K n for all n then H E K it follows from UC that the predicate R defined as in satisfies AR P gt AkK VQ Q k Pl k gt 7R Q This is because if gt R P F P Z G P then we can pick n with F P n Z G P n Setting k to be the greater of mp n and ma n the functions demonstrating UC for F and G then gives the right hand side of the above implication The above is the usual definition of the continuity property for predicates see Ros98 and says that the set of processes satisfying R is closed in the metric space Namely if z is a convergent sequence of processes in R then its limit is also in R Indeed a predicate is closed if and only if it is continuous these are just two ways of viewing the same phenomenon 3 Compactness is a strong property of a topo
6. a single model namely the failures divergences one making two further assumptions e We only consider predicates which exclude divergence which is as remarked above a straightforward simple refinement check e We use the model without the addition of v termination and therefore no process we consider can at the outermost level be capable of terminating via SKIP Let us call the divergence and V free portion of the failures divergences model M The whole model is generally termed M Ros98 The main reason for these restrictions is that they simplify the order theoretic properties of the model giving us the following proposition and reducing the number of special cases in definitions and arguments In particular it yields the following PROPOSITION 1 1 Each process P in N is equivalent to the nondeterministic choice of all deterministic processes that refine it namely Q Nt Q2 PA Q is deterministic Furthermore since this is in any case a practical requirement for FDR we will assume that the alphabet X over which processes are built is finite It also has the following mathematical advantages e All definable CSP operators become continuous in the standard order theoretic sense using the refinement order e Point set topology is important in the classification of properties over partial orders like CSP models there are various topologies over CSP models described in Ros91 Ros92 but as established in those pa
7. closed predicates and therefore could only be compared with our work in Section 5 It is also more restricted in that it only considers specifications of a single execution path universally quantified over all such Essentially an LTL predicate is a behavioural predicate on finite and infinite execution sequences The type of predicate dealt with in the present paper allows us to express predicates on sets of behaviours belonging to a process rather than just one of them Note however that since this is the nature of models based on individual process executions there can be no way of detecting exactly when some nondeterministic choice was made so we are not in the conventional branching time world either Finally the classes of predicates which are on the one hand refinement closed and on the other distributive have been thrown into focus by this work and the examples discussed above These should be the subject of future work Appendix Notation This paper follows the notation of Ros98 from which most of the following is taken Details of all the operators and models may be found in Ros98 URL given in the bibliography 13 Although there the atomic predicates talk only about performance of events not refusals To extend it to the latter requires at least the refusal testing model 20 A W Roscoe N natural numbers 0 1 2 gt Sigma alphabet of all communications T tau the invisible action
8. for a variant of the refusal testing model which as far as the author is aware has never been studied namely one in which there are infinite traces with infinitely many refusal sets interspersed 6 Conclusions In this paper we have shown as the author had long suspected that wide ranging classes of predicates on CSP could be expressed using refinement checking We have shown precisely which predicates are expressible using functions satisfying UC uniform continuity As ever answering one question raises others The previous section has gone some way towards answering the question of which predicates are expressible using more general functions but leaves quite a lot of gaps to be filled in A second issue is to gain more insight into the question of which predicates can be captured using finitary F and G ones which are finite state if their arguments are for these are the ones which are genuinely decidable using FDR Some recent work of the author on this question is reported in Ros04 A natural question to arise from this work is that of whether there is some interesting temporal modal logic which one could show was entirely captured by refinement checking This question has already been answered in the affirmative for LTL expressing properties in essence on complete and infinite traces essentially a type of extended behavioural predicate in LMC01 But that work is very different from the present paper It encompasses many non
9. in fact inevitable For example if Q and Q2 are incomparable processes under refinement the predicate Q E PV Q EP is not distributive even though the two disjuncts obviously are Suppose we are trying to represent a closed distributive predicate R Since our predicate is closed there must be a complete set Refr of refutations Y which characterise it from the definition of the 6 topology We can also assume that all are minimal in the sense that none is trivially implied by another refutation of R whether inside or outside Refr in the following sense We can write Y lt Y if 6 C P and NW Y In that case if failures P N Y then certainly failures P N Y So if Y is a refutation for R there is no point in including Y it is non minimal and it would be better to include only Y Note that this is not quite the same as assuming that the set of refutations Refg is itself subset minimal Claim that any minimal Y has lt 1 If not we can find one Y such that Y gt 1 Minimality of Y tells us that for each T C there is some Qr such that i R Qr and ii failures Qr NT YAT 6 The renaming is awkward in FDR because many extra channel declarations are required in general 12 A W Roscoe If this were not the case then T Y NT would be a refutation that implies Let G be the set of all T that have Y CT and T NY 1
10. neither the distributive nor refinement closed property which we will analyse later That however makes it a little contrived since the author cannot think of straightforward predicates which have a naturally useful interpretation and which have neither property EXAMPLE 2 1 Consider the following predicate on a process P Each trace s of P which has any extension has exactly two s z and s y with x and y being distinct elements of which may vary with s The proof of Theorem 2 1 would suggest we have to look at many distinct finite sets of traces modelled as the failures s to decide this all sets of the form s x whose intersection with P s traces must always have zero or two elements exactly But in fact we can do a lot better than this Imagine running three copies of P side by side making sure that they maintain the same trace by some mechanism until we choose to test them When we test them we must ensure that if there is any next event then the three copies between them have two but not three On firing up a test which will be done by a monitoring process M running in parallel with them we can get M to communicate twoevs if it detects there are two options at this point from two of the P s after the same trace and threeevs if three All we have to check then is that every trace of P that has a continuation can be followed by twoevs but never threeevs The following uses the very useful trick of double renaming
11. 8 The impossibility of things which a high level process with alphabet H transmitting information through a system P to a low level one with alphabet L is expressed as Ly P _ is deterministic where Ly P is the lazy abstraction operator which provides the view in X H L on the assumption that there is an arbitrary but unknown process interacting in an unseen way with P in the alphabet H Given that Ly P is defined in Ros98 to be the divergence free process whose failures are the stable ones of P Chaosy H H namely the failures generated at stable or r free states as opposed to ones introduced by divergence strictness it becomes straightforward to use Lazi s technique to convert noninterference a closed and refinement closed predicate into a refinement check just substitute the above representation of abstraction into the determinism check given earlier and use the failures refinement check of FDR The latter is done because it ignores any divergences which this syntactic representation of abstraction introduces In fact this representation of the noninterference check is arguably better than using the FDR determinism check implemented at the time of writing because it unlike the FDR one is never corrupted by one of these divergences Using the FDR determinism check on the process above will sometimes fail to find a result because of one of these though there are ways around this by using different representation
12. G P Go P R where s t could be replaced by any interleaving of s and t but not one of Chaos 4 F2 P R or Fi P Chaos 4 This is because for s t XM Y to be a failure of Q Q where Q and Q respectively have alphabets A and A2 we must have s X failures Q and t Y failures Q by the disjointness of A and A gt and our assumptions of X and Y This gives a contradiction proving our claim An alternative construction for disjunction over the traces model can be found in Section 5 as can a discussion of infinite disjunction 2 Here X and Y are ranging over subsets of the whole alphabet not just those of particular processes Indeed we assume here as we may that A1 C X and Ao C Y 4 A W Roscoe We note here because it will be of interest later that the constructions given here for both the left and right hand sides of conjunctions are distributive in P if all the F G are However the construction used for the right hand side of disjunction is not distributive since it involves putting two versions of P in parallel with each other Later we will see that this non distributive construction for disjunction is inevitable Uniform continuity Over the finite amp case that we are studying most CSP definable functions have the following property DEFINITION 2 1 A CSP definable function F is said to be uniformly continuous relative to a given model if for every leng
13. Q Ql EEP k gt R Q 10 A W Roscoe It follows that there is a finite set of failures namely failures P N s X s lt k U s 0 k such that failures Q 2 implies R Q is just the set of failures which are used in calculating P k But this is equivalent to having V in the proof of Theorem 2 1 which will now yield the function F for the left hand side of the refinement check if we are concentrating on this one set But this is just the constant function mapping every P to O e STOP We can now build the complete representation Refr of R as a collection of such s There is of course no need to choose the s that refute R P using just restrictions P k provided that for every P with R P there is one with C failures P AV Q C failures Q gt R Q and no other s than ones with this property Let S be a set of s that characterise R in this way Since we have the constant on the left hand side of our refinement check for every R all we need to do is to check that none of the Gg o P s can deadlock on the first step We can therefore dispense with the form of conjunction which uses separating traces and define for 4 Spec e STOP G P acs Ge a P which will generate a predicate equivalent to R Unlike the case where the different pairs Y were kept apart by different length traces this G P may not satisfy UC since it makes use of n
14. Theorem 2 1 to demonstrate that closed predicates can be represented as refinements uses failures refinement essentially even in the case where what is being tested is a trace predicate This was because we could use either traces or refusals to trigger the refusal of the event e and so giving rather than O but this would not have been possible in the refinement case if and O had differed in traces If we had been interested only in traces predicates earlier then it would have been straightforward to have used STOP and e STOP in modified constructions to get the same representation results as Theorems 2 1 3 2 3 3 and 3 4 In particular any refinement closed closed predicate would be representable by a check of the form STOP Cr G P in which G P can only take the two values STOP and e STOP If we have a countable collection of these predicates then it is possible to represent each of them like this or to modify the construction so that when the kth of them fails the resulting F P has the traces of nas k e STOP in other words it communicates k a s before a single e When it succeeds it only has the empty trace Now consider the process H P Fe P k N using the latter form of Fy which then has the traces of A E Hnas k e k N if and only if all the constituent refinements fail Hence STOP C AllTr 4 p H P is equivalent to the disjunction of the individual refinements Top
15. Under consideration for publication in Formal Aspects of Computing On the expressive power of CSP refinement A W Roscoe Abstract We show that wide ranging classes of predicates on the failures divergences model for CSP can be represented by refinement checks in a general form These are predicates of a process P expressible as F P E G P where F and G are CSP contexts and E is refinement We use ideas similar to full abstraction but achieve a stronger property than that Our main result is that topologically closed predicates are precisely those representable when F and G are both uniformly continuous We show that sub classes of predicates such as refinement closed and distributive ones are represented by special forms of this check Keywords CSP refinement topology full abstraction 1 Introduction The purpose of this paper is to classify the types of predicates which can be decided in its standard models of processes in the CSP process algebra using refinement checking The main motivation of this is to determine what can be achieved using FDR FDR which is a refinement checker for CSP The two main references for CSP are Hoa85 Ros98 Throughout this paper we will use the notation and conventions of the second of these the author s book This paper revises and extends a draft which was presented at AVOCS 03 Ros03 The main addition is Section 5 Both Hoare s use of P sat R where R is a property of behaviour
16. all CSP models See Ros98 for example The problem we have here is that there is no good reason why the right hand side of the above equation is in general a process which satisfies these conditions 8 To be even more devious one could use the same trick to code pairs by converting them into U 0 0 on the grounds that every process has the failure It is up to an individual as to whether to use this or not but we will implicitly do so when claiming that every distributive predicate can be expressed in forms and b 14 A W Roscoe e replacing P by a general context allows us to check any closed and refinement closed predicate e whereas replacing Spec by a general context and sometimes P by P allows us to check any closed and distributive predicate and finally e making both the left and right hand sides arbitrary CSP contexts allows us to check any closed predicate 4 Examples of distributive and refinement closed predicates This paper was inspired by the author s contemplation of a number of examples each of which was either distributive or refinement closed The crucial thing was that in each case it was possible to find a representa tion as refinement even where this seemed at the time unlikely We have already seen determinism above whose refinement representation was discovered by Ranko Lazi A closely related predicate is that of noninterference as specified in Ros95 Ros9
17. ble via a refine ment over the failures divergences or alternatively the little used traces divergences model e Any anti refinement closed traces predicate is representable via a failures divergences or traces diverg ences refinement It would be useful to extend the result about closure under countable disjunction to more than the closed refinement closed predicates However the author has been unable to find a construction which achieves this under the conventions established in this paper of using any potentially infinite CSP con struct over the failures divergences model However it is possible if we allow ourselves to move to the failures divergences infinite traces model U see Ros93 Ros98 This is arguably a more natural model given the types of infinitary constructs we tend to use but does of course take us further from the realms of practicality Consider the following alternative formulation of binary disjunction suppose we have a pair of refinements Fi P Er Gi P i 1 2 Then the process Gy P Gi P A reset Go P for reset a new event as before can perform any trace of G P a reset and then any trace of G2 P We can use essentially the same trick as we did earlier with and define FY P Chaosy reset A reset gt F2 P N Fi P A reset Chaoss reset Essentially the same argument used with the interleaving version shows that Fy P Er Gv P is equivalent to the disjunct
18. but no P with R P is refuted by any member of Ref then we will call it a a complete set of refutations for R A given predicate R may have many such sets representing it So Refr is a complete set of refutations for our R For example in the case of the predicate R P Q E P a complete set of refutations is f f f Z failures Q For the time being let us concentrate on a single refutation Y which is one member of a complete set Ref representing R Then failures P N Y implies R P We can try to construct Fg y and Gav such that Fev P E Gaa P if and only if failures P N 4 Y One way of approaching this is to aim for the following 4 The topologies defined in those papers are actually over possibly infinite product spaces of processes Since for the time being at least we are only interested in predicates of single processes our definitions are a little simpler In any case the significant differences in considering product spaces only appear in infinite ones which are most unlikely to be of practical interest in refinement checking 6 A W Roscoe e Make Fo P and Ge P always equal one of e gt STOP and E e STOP N STOP for e any fixed event outside the alphabets of the processes P we are considering noting that strictly refines oo e Make Fs 4 P equal if and only if failures P contains no element of Y Equivalently failures P M BCW e Make Gs P equal
19. e free we need only consider a predicate is closed if and only if whenever R P there is a finite set such that for any Q if failures P N failures Q N then R Q For example the predicate defined R P Q E P for any fixed Q is closed because R P implies that there is f failures P failures Q Evidently if failures P N f failures P N f then 4R P so we can set f In our finite alphabet case this topology coincides with the metric one since there only are finitely many failures and divergences with traces of length less than any chosen k But the above restricted to failures because of our initial assumption that we are only considering predicates of divergence free processes gives the following useful representation of closed predicates noting that a predicate is closed in this topology if and only if it is closed in the metric one Choosing for every P such that R P and setting Y N failures P it follows that if R is a closed predicate then there is a set Refr of pairs Y of finite sets of failures with Y C such that R P V Y Refr failures P N AU This observation leads to the following definition DEFINITION 2 4 If for a predicate R WV is such that V P failures P 1 Y gt AR P then we say that W is a refutation for R If Ref is a set of refutations which is sufficient to have a Y Ref refuting every P such that 4R P
20. e is no hope of expressing it in CSP We can however do an equivalent trick let e be an event not appearing in P or and consider P P OneF where X e OneE 2 5 e gt OneE O STOP N e gt STOP P C P so in particular P has all of P s failures The big difference however is that we can remove any failure s X U e without harming the model axioms and so we can let PxC failures P s X U e s X ec A s X A failures P and this always is a process It removes from P just those s X U e for which the complete set C of refutations says that s X may not be in P This means we can check our predicate via the refinement PCCP t Of course this is just one possible trick for expressing the predicate of C as a refinement And to use it we still have to implement P C So how can we build PxC Obviously it must have all traces of P with the possible addition of e and nothing further after each of them We must give it all the failures of P aside from refusal of sets including e and we must allow the presence of sets involving e to be influenced by C and its observations of failures P One way of achieving this is by the parallel composition P Il Q Chaos y OneE Z e xu where Q is a process whose traces include those of P and whose failures on each trace are a subset of those of P if the trace is one of P If Q does no
21. es it should perhaps not come as a great surprise that we seem to be able to express richer predicates in it An interesting question that arises is whether one can express over it the countable disjunction of predicates based on both finite and infinite traces there being no hope for refusals because the arguments above still apply Certainly the above idea does not work even for pairwise disjunction as the construct never combines two infinite traces into a single one The interleaving based pairwise disjunction from earlier in this paper does work however The author believes it is possible to give a countable disjunction using a combination of the ideas in these two methods but the result is even more esoteric than the ideas we have seen before Simple infinite interleaving will not work because i this construct is itself inadmissible like all infinite parallel operators in CSP and ii the actions of individual processes cannot be distinguished without using an infinite alphabet If on the other hand we use the same idea as in our second treatment of determinism checking earlier and use Clunk F P and Clunk G P then we can control the order in which the processes perform actions For example we can create a process in which e Any non clunk action immediately before the kth clunk is the jth action of process i where i j is the kth member of an enumeration of N x N If there is no such action then this process will never be permitted
22. f P and then force the second to accept it If this is successful it does the same again otherwise P was nondeterministic To implement this we run P a a 1 a A and Pla a 2 a A similarly to the example where A contains all events of P interleaved and put them in parallel with Monitor 2 1 A 1 2 2 Monitor and the monitor interface MI A 1 U A 2 In this the Spec to refine G P against is just the specification that G P never deadlocks on an odd length trace with this formulation also taking into account that A 1 and A 2 events always alternate Spec STOPN Kickers a l Spec Sped Fea a 2 Spec On the expressive power of CSP refinement 11 This implementation of determinism testing different from the one used by FDR which is non monotonic and outside the scope of this paper was invented by Lazi Laz98 That representation was the starting point for the work in this paper One can modify this test for determinism to avoid the renaming choose an event clunk not used by P and define Clunks x X clunk gt clunk gt Clunks Clunk P P Clunks X clunk Repeat z X clunk gt x Repeat DetTest Clunk P Clunk P clunk Repeat clunk x and this will also deadlock on an odd length trace just when P has a nondeterminism Since we can make processes like M and Repeat monitor the behaviours of various copies of P on different traces as well as when t
23. h can perform any sequence of P s traces separated by reset s and AllTr g P TRSgQ Resettable P b gt 9 This follows from the continuity of all operators over the subset order on the stable failures model F of CSP see chapter 8 or Ros98 16 A W Roscoe AllTrg P can diverge if and only if P has all of Q s traces or in other words if P fails the predicate Therefore testing if this context of P refines STOP the only value other than div for a process with all events hidden decides our predicate which is the negation of the closed PErQ This example shows clearly how we can put infinitely many behaviours of P into a single divergence of AllTr g P There is no analogue of this construction for failures or divergences For these reasons we will consider only trace predicates in the rest of this section namely ones which are determined by the set traces P of P s finite traces We saw earlier in this paper how to express binary disjunction of two failures predicates by means of doubling the events and using interleaving There is no way in which this approach can work for infinite disjunctions because e it would require an infinite alphabet which we have excluded and more importantly e infinite parallel operators are not properly definable in CSP since they cause great theoretical problems Let us consider the disjunction of refinement closed closed trace predicates The construction used in the proof of
24. her can contain any member of f meaning that the one containing f fails R In either case we have aR P N Q gt 7R P V AR Q which is logically equivalent to R P A R Q gt R P T Q namely distributivity A slightly altered form of this argument also works for infinite nondeterministic choice If Refr contains only members of the form then R is closed under anti refinement not such an intuitive concept as being closed under refinement On the other hand if it contains at least one of the form f then it is not by minimality of the members of Refr and a simple argument Notice also that unless Ref contains at least one f with f then Chaoss the refinement least element of N will satisfy R A simple refinement specification which is distributive as observed earlier is precisely one that can be represented by Refr containing only pairs of the form f f Just as the concept of k boundedness was so important in the representation of refinement closed predi cates as more convenient refinement checks it should not be surprising that the shape of Refr plays a large role in the representation of distributive ones It is cleaner to separate out Refr into two sets C being all the pairs with empty Y and C2 being those with singleton Y We can then verify R by two refinement checks one for each So consider first the case of a collection C Ci say of pairs with empty W It is a corollary to the
25. hey are constrained to act the same it follows that the technique can simultaneously look for all misbehaviour in any k bounded representation of a refinement closed predicate using k interleaved renamed copies of P Of course unless the resulting M is itself finite state the implementation of the predicate will not be either but the fact that P is used only k times means that M is the only possible source of infinitary behaviour In the case where M is finite state with M states say then the overall complexity of the refinement check is bounded by M N where P has N states 3 2 Distributive predicates Any predicate that can be written R P F P C G P with G distributive is itself distributive since if R P and R Q then F PT Q E F P 1 F Q by monotonicity of F F P NF Q E G P N G P by R P A R Q and properties of partial orders and G P N G Q G P N Q by distributivity of G It follows that R P M Q holds We might hope after our experience to date that any distributive predicate can be expressed in the above form It is interesting here that we do not require F to be distributive for R to be Remember our earlier construction to represent the disjunction of two predicates Since the disjunction of two distributive predicates is not in general distributive the connection shown above between distributive G and distributive predicates shows that the non distributive G remarked on earlier involving interleaving is
26. ich a process P can satisfy anything like a functional specification and some refinement P does not requires explanation since P is permitted to behave exactly like P The proposer must answer the question of why it is reasonable for P to satisfy the specification if the totality of its actual behaviour does not And in many cases we would expect that if P and Q both satisfy a specification then the process which behaves like either one of them also satisfies it The following theorem demonstrates that these two properties together reduce a specification to a well known case a satisfiable predicate is one which is satisfied by at least one thing it is not equivalent to false THEOREM 3 1 The satisfiable predicate R is refinement closed and distributive if and only if it is expressible as a simple refinement check On the expressive power of CSP refinement 9 Proof Suppose first that R has these properties Let y R R where R is identified with the set of processes satisfying it then x R R by distributivity and y R E P implies P R by refinement closure It follows immediately that P R if and only if P 3 y R as required Conversely if R P is specified by P 3 S the proofs that it is satisfiable by S refinement closed and distributive are all trivial What we will do in this section is to consider predicates which are either refinement closed or distributive and how they might be represen
27. ided by refinement checking is of the form R P F P EG P ft where F and G are both CSP contexts i e process expressions which may involve the process variable P The most general predicates are then logical combinations using A V of these For practical purposes we should restrict ourselves to combinations of a finite number of these basic predicates each of which has the form that F P and G P are always finite state when P is otherwise deciding the predicate would generate an infinite amount of work for FDR However this paper explores well beyond this practical domain Most of our effort will be spent on basic checks of the form in f It is natural to identify each predicate with the subset of M consisting of those processes satisfying it We will often make this identification Conjunction and disjunction Before we study how to represent individual predicates it is interesting to show that one can represent both conjunctions finite and countably infinite and finite disjunctions using refinement checks alone In other words one of these logical combinations of refinement checks can be represented as a single refinement check Suppose first that F P E G P are all representations of predicates R P Then if we pick new events a b consider the processes F P nas n 6 Fn P and G P 1 nas n b Ga P where nas 0 c c SKIP nas n 1 c a nas n c It is not too hard to see that F P E G P
28. if and only if F P E G P for all i since we know instantly by looking at a trace which of the F P or G P it relates to unless it is a trace consisting only of a s on which the two sides have identical behaviour The single refinement will only hold if all the constituent ones do and vice versa It is trivial to cut this down to a finite conjunction but it cannot be extended from these uncountably infinite conjunctions to uncountably infinite ones without an uncountable alphabet which we do not have For disjunction at least over the failures model we need to extend the alphabet further Given the refinements F P E G P for i 1 2 choose an injective renaming R extending the alphabet if necessary such that F2 P R and G2 P R have disjoint alphabets from both F P and G P Note that applying an injective renaming to both sides of a refinement test never changes the outcome Call the resulting alphabets A and A2 The refinement Chaos 4 F2 P R n Fi P Chaos ay Gi P G2 P R is then equivalent to the disjunction of the two parts If either refinement does hold then by construction the above holds as Chaos is minimal amongst divergence free processes with alphabet a subset of A If it were to hold and neither constituent does then we can find failures s X t Y respectively of G P and G2 P R which do not respectively again belong to F P or Fo P R The failure st X N Y is one of
29. if and only if failures P contains every element of Y This is equivalent thanks to our assumption that U C to failures P N D WV Note that these specifications of Fg y and Ge y are both monotonic and indeed both metric and partial order continuous meaning that they are reasonable things to aim to represent via CSP syntax Importantly refinement only fails when Fg P O and Gg P E namely exactly when failures P N Y Let us first consider how to build Fg P What we would like is that it always has the initial capability to communicate the event e and only e but can only deadlock on the first step if failures P contains any element of Y Let s X be a typical element of this set We define a testing process for it as follows T X z X gt e STOP Tayu X a gt P u X e STOP Test s X P T s X P N e STOP where X is the set of all events other than e Since T s X only has finite traces the hiding can introduce no divergence It is obvious that the only possible traces are e and and that on the empty trace Test s X P can only refuse e when its T is in state X This is when it and P have each performed the trace s but the combination then will only deadlock if P is refusing all the events in X In other words the combination can deadlock on the empty trace precisely when P has the failure s X If we now define Fo 0 P l e STOP U Tes
30. ion of the two constituents This does not work for failures since the refusal at the end of the first process s trace is ignored It is possible to extend this to countable disjunction but only if we use a model which admits infinite traces For a sequence P P i N of processes we define Il P head P A reset II tail P 18 A W Roscoe to be the process which performs one trace of each of the P in sequence separated by reset s Suppose we are given sequences of functions F i N and G i N whose refinements over U represent a sequence of finite trace predicates where any failure of refinement would show up as an illegal finite trace of the right hand side We can then define S to be the sequence of processes which is Chaosy reset except at position i where it is F P P being the process we are checking for the disjunction of the implied predicates and I G P i N Then Chaoss I 1 I1 S LE N Cy I T if and only if any one of the constituent refinements F P Er G P holds The if part is trivial for if Chaosy Fi P Cy Gi P then a Chaoss T S Eu H I For only if observe that if none of F P Er G P holds then we can find finite traces s of G P which are not possible for F P The trace so reset s reset is then a trace of II I which is not a trace of any of the constituents of the left hand side of the refinement abo
31. l the processes which perform n a s and then a b but not by the limit of this sequence the process that performs a s for ever Once we try to extend beyond the world of closed predicates it seems to be the case that the expressibility of predicates on finite traces and refusals starts to differ For example we saw above that the predicate can communicate b a trace property can be expressed as a refinement However a similar failures predicate there is a trace s after which b cannot be refused is not expressible For suppose it were expressed by F P E G P Consider the processes B which can refuse b after any length of trace of b s and By which can do the same except not refusing b after k b s Plainly we must have F B E G B but not F B E G B The failure of refinement must be in refusal sets since the traces and divergences of F B must be the same as those of F B and similarly for G It follows that G B must have some failure s X which is not in F B and hence a not in any F B as these all refine F B and thus b not in G B for any k either We can be sure that s is a trace of both sides but not a divergence It is a property of CSP operators that whenever s X is a non divergent failure of H P then there is a finite set of failures of P such that s X failures H Q whenever C failures Q It follows that s X failures B is proved by some finite set of B s fail
32. logical space which says in a fairly strong sense that the whole space is bounded In a metric space as we have here compactness is equivalent to there not existing an infinite set D of points with no limit point namely a point z such that for every e gt 0 there are infinitely many points of D within e of z On the expressive power of CSP refinement 5 Representing closed predicates We have thus shown that all predicates representable by using UC F and G are closed Our main result is going to be the reverse of this showing that all closed predicates are expressible using t using F and G which satisfy UC It is helpful to turn our attention from the metric space to one of the other topological views of CSP from Ros91 Ros92 namely the 6 topology DEFINITION 2 3 The 6 topology on N is defined by specifying that a set C C N is closed if and only if whenever P C there exist finite sets of failures and A of divergences such that for all Q failures P N failures Q N A divergences P N A divergences Q NA gt QC A topology is defined by its set of closed sets Note that unlike the metric one the 6 topology is not based on lengths of traces The reason we use the latter here is that it allows us to understand closed predicates in a rather intuitive way as we will see This is especially important when we come to study distributive and refinement closed predicates For N where all processes are divergenc
33. n first Running P in parallel with itself is more general and in any case the sequence idea is not very useful where we cannot have termination so we will concentrate on P in parallel with itself Recall the structures of the F and G used in the proof of Theorem 2 1 the distributive function F P uses many instances of P but they are all on distinct execution paths no sequence of actions of F P invokes any more than one of them in parallel On the other hand G P interleaves multiple copies of P which leads to it not being distributive To see why this happens consider H P P P and observe that if P a P and Q b Q then H PN Q H P N H Q since the left hand side contains traces with both a s and b s whereas the right hand side does not What we now do is to prove what was hoped for at the start of this section THEOREM 3 2 Every closed and refinement closed predicate can be expressed in the form t Proof If R is such a predicate and R P we know that there is k such that VQ Ql k P k gt 7R Q Now suppose R Q holds and Q k E P k The construction failures Q s X failures Q s lt k A s X failures P Viu u s wv ul kAu traces P then builds a process that refines Q and for which Q k P k This is a contradiction since we can deduce R Q from the equality of restriction and R Q by refinement of Q Therefore the same value of k actually yields V
34. ologically speaking this actually implies that all refinement closed open sets of the traces model i e the complements of closed sets are expressible For every refinement closed open set U is the union of the closed and open clopen sets P PAE F for those finite F and n such that the above set is contained in U Since there are only countably many of these basic clopen sets it follows that every open set is the union of countably many closed ones For the rather less useful category of anti refinement closed trace predicates we can get a similar result 10 It is of course natural that we should be able to judge trace predicates by means of trace refinement However bear in mind below that we will make critical use of divergence to help judge trace predicates and that in these cases we need trace plus divergence refinement which can easily be judged in the failures divergences model If the presence or absence of refusal sets were an issue which it will typically not be below since we hide all events then parallel composition with Chaosy on the left hand side of the refinement gives the proper meaning 11 These sets are topologically speaking a basis 12 If Q is in U then the processes Q Tn QU st s E QA s n At d are a sequence that converges to it therefore one of them is in U and all that Q T n s refinements are too On the expressive power of CSP refinement 17 We know from earlier discussion tha
35. ommunicates threeevs What we actually now require is that TT P and CN P are trace equivalent this is easily testable via two refinement checks or indeed one if we form a binary conjunctions by prefixing the two sides with different events here a and b and test a TT P 0 b gt CN P Chaoss a gt CN P 0 b TT P Chaosy The Chaosy s make sure that the refinement ignores refusals Note that this binary conjunction uses a simpler recipe than the countable form described earlier This particular predicate is neither refinement closed because a refinement can reduce two continuations to one nor distributive since M can increase the number of continuations We were able to make this check finitary because of the way that all the behaviours we were comparing at any one time always come from the same arbitrary trace These things are not essential for example we could use any finitely computable property of traces to tell us which to look at but they certainly help The topic of exactly which predicates may be captured with F and G both finitary remains one for future research though some progress is reported in Ros04 3 Distributive and refinement closed predicates We will now look at two special cases namely refinement closed and distributive predicates of N as defined in the introduction These are both natural attributes for useful CSP predicates to have any instance in wh
36. ondeterministic choice in a way that can potentially map arbitrarily long behaviours onto the initial deadlock Of course if UC were required one could revert to the use of a s and b s If we can bound the size of the sets giving a measure of how many different behaviours we need to observe at once to refute our predicate R then a simpler and more practical form of predicate can be found A set of pairs I which characterises a predicate in the sense of Theorem 2 1 will be said to be k bounded if each Y is no larger than k This is rather more striking for the representations used in Theorem 3 2 since each R P can be detected by observing that one of a selection of bounded sets is a subset of P An excellent example of this is the determinism condition described in the introduction this fails just when P has the failures s a and s a 0 for some s and a So this predicate is 2 bounded and every failure of it shows up in P having an offending pair of behaviours The way to test for this is to run two copies of P together with separated alphabets and ensure that one of them cannot refuse an event that the other accepts on the same trace This suggests the model of running the two copies interleaved probed and tested by a monitor process that observes their behaviours and flags errors The best way of testing in this way for determinism is for the monitor M to accept any event from the first copy o
37. pecifications Proceedings of CPA 2004 IOS Press
38. pers they all collapse to the same one when is finite this has numerous useful properties such as compactness We will however feel free to add finite collections of events to our alphabet for the purpose of expressing predicates The rest of this paper is structured as follows In the next section we will prove a general theorem the main one of this paper that shows that an unexpectedly large class of predicates are all expressible as refinement checks In the following sections we look at two important subclasses of predicate namely refinement closed ones and distributive ones which each have distinctive styles of representation and which in the author s experience constitute most practical predicates that are not behavioural We consider various examples of these two classes which are formally defined DEFINITION 1 1 The predicate R is refinement closed if and only if R P and P E P implies R P Namely if P satisfies the predicate then all its refinements do R is distributive if and only if whenever S is a nonempty set of processes satisfying R then R 1S On the expressive power of CSP refinement 3 Finally we examine what can be achieved if we allow our representations to make use of divergence For reasons which will become apparent we concentrate mainly on traces predicates in that section There is an appendix of CSP and other notation 2 General predicates The most general basic predicate that can be dec
39. predicate of the form Spec E P for P the process we are checking and Spec fixed a simple refinement check Of course the large number of applications of behavioural predicates and that fact that functional specifications are naturally of this sort suggest that most practical predicates one will wish to prove will be behavioural However there are more sophisticated specifications which can not be so expressed usually ones which judge combinations of a process s behaviours rather than individual ones The classic example of this is the extensional notion of determinism from the failures divergences model e P must be divergence free and e if P has trace s a then it does not have the failure s a P cannot have the option either to accept or refuse a In fact for technical reasons this second condition implies divergence freedom The first clause of this can be checked by refinement against the most nondeterministic divergence free process Chaosy but the second cannot A striking way of seeing this is to observe that every predicate of the form P 2 Spec is distributive if P and Q satisfy it then so does PM Q but it is self evident that determinism is not distributive We will see later that in common with many other such predicates though determinism is not checkable via a simple refinement check it is decidable using a refinement check of a more elaborate sort In Sections 1 4 of this paper we will concentrate mainly on
40. proof of Theorem 2 1 that the following theorem below holds Each Gig is the constant meaning that if Ref is infinite then the G produced by the proof of Theorem 2 1 is the process S which performs any number of a s nondeterministically one b and then equals If C is finite then the same S will still work with F P being the process formed by a selection of the ab traces being followed by one of the F g 9 P s as varies over C all the rest being followed by Alternatively when C is finite one can choose a simpler and finite S THEOREM 3 3 The closed R is anti refinement closed or equivalently can be refuted using a set of pairs Y such that all U s are empty if and only if R F P CS b for some CSP definable F satisfying UC and fixed process S Furthermore in the only if case we can choose F to be distributive For C C2 consisting of pairs with singleton Y we observe that a process satisfies the equivalent predicate i e the one for which C is a complete set of refutations if and only if failures P failures P f X f CA X N failures P 9 On the expressive power of CSP refinement 13 and that this really only means testing left to right inclusion If we could express the right hand side as a process then this would be a refinement check But the right hand side is not necessarily a process since it may well not satisfy the model healthiness conditions meaning that ther
41. re considering only a finite alphabet however means that there are only at worst a countable infinity of them and so we can list the whole of our set Ref Bo Vo Y s where the indices range over a set I which is either some 0 n or the set N of natural numbers Obviously there is no need to worry about the case where I is empty since then the predicate R is true We simply appeal to the ability demonstrated earlier to represent the conjunction of a countable family of refinements and the entire closed predicate is represented On the expressive power of CSP refinement 7 Though this construction uses unbounded nondeterminism the resulting F and G do in fact satisfy UC because of the traces a a a 6 that are introduced there are only finitely many refutations that are relevant to traces of any given length in the resulting F P and G P We can conclude the following THEOREM 2 1 The predicates of N which are closed in the metric topology are precisely those that can be expressed as a refinement F P E G P in which F is distributive and where each of F and G satisfy UC but where the constructions of F and G are in general infinitary Now consider the function H P a F P N b gt G P where F and G satisfy UC and represent the predicate R Since the set of processes C a gt QTd gt Q QC Q is closed and H C is precisely the set of processes satisfying R we get the following result
42. s of the predicate A second predicate is that of fault tolerance as formulated in Ros98 for systems in which errors are triggered by some events that are assumed to be in the hands of some demon rather than ordinary users One advantage of this approach is that it allows assumptions to be made on the number frequency etc of errors thanks to parallel composition of the system P with some error regulator creating an overall system Preg A second is that it gives a very elegant characterisation of fault tolerance P STOP E L2a Preg E where F is the set of fault events This simply says that the system with faults permitted but abstracted is a refinement of how the system behaves when there are no faults Intuitively this is similar to non interference since it says that error events do not significantly affect what the user sees It is however a different predicate since it allows errors to cut down the nondeterministic range of behaviour and indeed allows nondeterminism much more freely in general Unlike noninterference it is not refinement closed but as the form of the above definition shows given our earlier analysis it is distributive which noninterference is not The right hand side will always be a distributive context as the regulator process if any should not involve P A little transformation easily converts the above into the form 4 in the case where Preg P P STOP Chaosg E P E More recently
43. s rather than sets of behaviours and the fact that FDR is the only widely used verification tool for CSP have tended to concentrate the language s users on so called behavioural predicates namely ones which are judged true of a process when and only when all the process s behaviours traces failures divergences are acceptable Every specification of the form P sat R can be checked by testing if P refines the characteristic process of R namely the nondeterministic composition of all processes Q such that Q sat R Furthermore the most natural style of using FDR is to check that Spec E P for some Spec representing the predicate being asserted In the second case FDR process P passes just when all its behaviours are ones of Spec since refinement is defined to mean reverse Correspondence and offprint requests to A W Roscoe Oxford University Computing Laboratory Wolfson Building Parks Road Oxford OX1 3QD UK email Bill Roscoe comlab ox ac uk 1 A predicate is simply a condition that maps a process to true or false in other words a property of processes The reason why we use the term predicate in this paper is to distinguish linguistically the properties of processes we are trying to characterise from the many other uses of the word property in this paper 2 A W Roscoe containment over behaviours Of course in both cases the precise types of behaviours checked will depend on which CSP model is used Let us term a
44. t any anti refinement closed closed predicate can be represented in the form F P CS However it is clear that if we are simply restricting ourselves to traces predicates then the refinement above can be trace refinement This gives us an opportunity to transform it into the form AllTrg F P E div judged over the failures divergences model M since the left hand side diverges just when P has all s traces Now any nonempty set of such refinements F P ES A A can be disjoined PI AllT rs F P E div This is the disjunction since the refinement plainly holds precisely when the left hand side can diverge on which is equivalent to at least one of the constituent refinements being true This trivially implies that all anti refinement closed trace predicates are expressible whether open closed or neither We can summarise the above results plus re statements and easy re workings of some from earlier in the paper as follows THEOREM 5 1 The following hold for traces predicates e All closed predicates can be decided by f using traces refinement Cr using functions satisfying UC We can similarly replace by Er for the other results of Sections 2 and 3 namely Theorems 2 1 2 2 3 1 3 2 3 3 and 3 4 e The classes of traces predicates representable are closed under countable conjunction and finite disjunc tion e Any countable disjunction of refinement closed and closed traces predicates is representa
45. t have the failure s X U e which is achieved by making Q always offer e when it refuses X after s then the above combination does not have the failure s X U e but since P does if s X is a failure of P the refinement would then fail So we would want Q to have the failure s X U e only if all of the s X C with this failure have at least one member of s X in failures P This can be achieved less clumsily in the case where the number of f with a given f is bounded but not in ways which seem to the author to lead to likely practical implementations It is appropriate to widen the specific check 4 above to the more general one below which is closer to our previously named styles THEOREM 3 4 Every distributive closed predicate on N can be represented by a check of the form F P E P b where P is as above and F is a CSP context In practice it is often possible to simplify this form with P becoming P It is an open question whether it can always be simplified like this It is of course interesting that distributive predicates can be expressed in this form Notice that we have now proved the following e Starting from the observation that every behavioural predicate i e one which is refinement closed and distributive can be expressed as a simple refinement Spec E P T Such conditions for example the prefix closure of the traces of a process are common to
46. t s X P s X amp U it follows that we have exactly the function we want which is finite state because is finite The nondeterminism here means that we are running the various tests T s X as alternatives if any one of them gives value then this disjunction does The function F g y P is distributive over M since each particular run of it uses P at most once this will be of interest later The situation with Gg y P is somewhat different since in order for it to deadlock on we require P to have every failure in Y We can fix this by replacing the nondeterministic choice above with interleaving Geu P STOP Me gt STOP Illve xyew Test s X P e STOP e If P fails to have any one of the selected failures then since the appropriate component of the interleaving above cannot refuse e on the empty trace neither can the whole interleaving If it does have all of Y then it can but will certainly have the trace e The second line makes sure that nothing can happen after the first e so that it always equals O or Z So this definition does what we want it is not however distributive since Y copies of P are run in parallel Indeed we shall see later on that there is no hope of Gg y being distributive Therefore we have the F w and Ge y we wanted to represent a single refutation In order to check an arbitrary closed predicate however we may need to check an infinite number The fact that we a
47. ted 3 1 Predicates that are refinement closed Since each CSP context F P and G P is monotonic with respect to P it follows immediately that whenever F P is constant not depending on P then the check f is refinement closed It is therefore reasonable to speculate after the result in Theorem 2 1 that every closed and refinement closed predicate can be expressed in this way Since the notation F P with F constant is a little confusing we will in this subsection consider refinement checks of the form R P Spec E G P It is well known that all standard CSP operators other than recursion are distributive in each of their arguments separately A context H is distributive if H P N Q H P n H Q for all P and Q and more generally H 1S T HH P P S for all nonempty sets S of processes If G is distributive it follows that the R P of f is itself distributive since if G P J Spec for each P S then G I18 1 G P P S 3 Spec Note that in this case we can deduce by Theorem 3 1 that the specification given us by can in fact be written in the form Spec E P a simple refinement It follows that in order to get any increase in power we need to look at non distributive G P A context will typically be non distributive if a single behaviour of G P depends on more than one behaviour of P which will be because P is either run in parallel or in sequence with itself possibly being operated o
48. th of trace k there is another length m k such that for all processes P Pim k Q mk gt F P Lk F Q Lk UC where P n behaves exactly like P until n events have been performed and then diverges see Ros98 In other words the behaviour of F P up to step k is completely determined by the behaviour of P up to step m k This definition is similar to but much weaker than those of the familiar CSP concepts of a constructive or non destructive function see Ros98 The only exceptions to UC for CSP definable F and finite are e When F may introduce divergence through hiding i e F P can diverge when P does not This does not exclude all uses of hiding provided the structure of F guarantees that no consecutive infinite sequence of events will be hidden In fact we will use such safe hiding often in the F s and G s we build e When unbounded nondeterminism creates a choice between an infinity of processes which have for a fixed k arbitrarily large m k s From the standpoint of mathematical analysis UC is closely analogous to uniform continuity with respect to the usual metric on the model d P Q inf 2 P k Q Lk A function from one metric space A d to another B dz is said to be uniformly continuous if for all gt 0 there exists 6 gt 0 such that for all x and y in A di x yY lt 6 gt do f x f y lt See Ros98 Ros92 Ros91 for details on metric spaces over CSP models
49. the author was presented with two predicates representing correct interaction between client server pairs developed by Joy Reed and Jane Sinclair Here it turned out that one was distributive but not refinement closed and the other which is its weakest refinement closed strengthening is not distributive On the expressive power of CSP refinement 15 His experience in representing these as refinements was similar to that for the above examples as is reported in RSR04 Some further examples of natural non behavioural specifications can be found in Ros04 5 Divergence and related matters We showed earlier Theorem 2 1 that any predicate represented using t for F and G satisfying UC is topologically closed We also observed that hiding either coupled with infinite nondeterministic choice or used in a way that might introduce divergence had the potential to create functions not satisfying UC They can certainly create predicates that are not closed consider STOP E P a b T H P nupto n bD 2 b n EN E b STOP where nupto n b is a process that does n events and stops and additionally stops after communicating b The first of these refinements specifies thanks to K nig s lemma and being finite that P has only finitely many traces all of which consist only of a and b The second says that P can communicate a b at some point Both of these predicates fail to be closed for example each is satisfied by al
50. the copies of P so that as well as following events by their usual 5 In fact the best way to regard our result is as a higher order form of full abstraction The usual definition of at least the main part of full abstraction is that whenever two processes are distinguished by some model then there is a simple test on some context of the processes that distinguishes them What we have here is a proof that given a closed set of processes we can used the same pair of contexts to distinguish between all pairs of processes inside and outside the set 8 A W Roscoe names they each have a separate tagged copy CN P rn 1 P ra 2 P rn 3 P A A I M A 1U A 2U A 3 AUA 1UA 2UA 3 m i P Pllaca a a il ae All M 22 A gt M 1 Al y 2 A2322 3 A3 card x y z 2 amp twoevs STOP card z y z 3 amp threeevs gt STOP II Note here that all three copies of P keep in synchrony until the first one communicates in its alternative copy alphabet A 1 with M which then tests to see what events the other two can do The copy alphabets are hidden so we only see ordinary events plus the two signals To test the requirement we can cook up a slightly simpler process along the same lines TT P ra 1 P M a 1 twoevs a A AUA 1 M P xz A M P a 1 A 1 STOP So for each trace s a of P we have the trace s twoevs in TT P but it never c
51. to communicate again This allows us to compare the constituent refinements action by action without having an infinite alphabet e The ith process is only started up by some appropriate recursive structure once it is actually allowed On the expressive power of CSP refinement 19 to perform actions This will mean that at any time there are only finitely many processes running in parallel The details are left to the interested reader Returning briefly to the issue of failures recall that one of our difficulties in combining failures specifi cations is that each failure only contains a single refusal set Just as with the move from finite to infinite traces it seems that there is a richer model where things may be easier This is a model called the refusal testing model Muk93 based on earlier work by Phillips Phi87 where refusal sets are recorded throughout the trace rather than just at the end This means that constructions like the second version of binary disjunction will now work over this model which since it is more expressive than the failures divergences model M can certainly express any predicate that M can However since it is still of course the case that refusal information does not contribute to traces or divergence information under any CSP operator there is no chance that we can perform tricks using divergence like AllTrg P which tell us anything about refusal sets Therefore there would be more need than with traces
52. ures which means that it belongs to G B for sufficiently large k This contradicts what we already know It follows that this predicate is not expressible via t Note that this is the first such example we have seen The author has identified two reasons for the comparative difficulty in expressing refusal predicates The first seen above is that since refusals are only ever used to calculate other refusals we cannot make use of for example divergences to give us extra leverage The second is that we can only look at one refusal set per trace and this is of uniformly bounded size thanks to the finite size of X This is in contrast to traces where we can string an infinite collection together and then hide them As an example illustrating the power of combining an infinite set of traces into one consider the predicate Q has a trace which is not a trace of P for any fixed Q We can assume Q has an infinite necessarily countable set of traces since otherwise it is a closed predicate and therefore representable Since Q has a countable set of traces we can enumerate them t t2 and build a process TRSg which performs these traces in this order putting an extra event reset after each For example if Q can do any number of a s then TRSg might perform no a s reset one a reset two a s reset three a s and so on Now consider the construct taken from Hoa85 Resettable P P A reset Resettable P whic
53. v tick the action representing successful termination A set of all length n sequences over A A set of all finite sequences over A AY set of all infinite sequences over A the empty sequence 1 the sequence containing a an in that order a the infinite trace a a a st concatenation of two sequences s X hiding all members of X deleted from s s xX restriction the members of s that are in X which share members of X and are disjoint elsewhere s lt t Ju su t prefix order equality between boolean expressions and predicates Processes STOP the process that does nothing SKIP the process that simply terminates v successfully Chaos 4 the most nondeterministic divergence free process over A C X div the process that does nothing but diverge equivalent to div M Chaoss in M up P recursion a P prefixing x A gt P prefix choice b amp P conditional execution equals if b then P else STOP POQ external choice PNQ 1S nondeterministic choice P allp Q alphabetised parallel PQ generalised parallel P and Q synchronise on X x P l Q interleaving unsynchronised parallel P X hiding P R renaming relational PrQ time out operator sliding choice PAQ interrupt Pla y substitution for a free identifier x Pin The least refined process which behaves identically to P for n steps In M it diverges unless P already has after every length n trace of P d P Q metric distance between P and Q
54. ve The fact that we need to assume that the constituent refinements are themselves judged over U is not a damaging restriction since all of the constructions used earlier would have worked equally well over the more elaborate model Observing that any open predicate over the traces model is the countable disjunction of clopen ones since there are only countably many clopen balls of the form B r y x d x y lt r in total d being the metric with the same definition as earlier but based on the standard restrictions P n over the trace model T rather than M and therefore representable using the above and Theorem 5 1 we get the following result THEOREM 5 2 The following are representable as refinements over U a Any countable disjunction of trace predicates representable as refinements over T b All open traces predicates Unlike the construction involving AllTr g P above it does not appear to be possible to map this infinite trace refinement down to the failures divergences model by using hiding to create divergences The reason for this is that the left and right hand sides of our refinement are too complex and in particular there are potentially uncountably many different counter example traces which might be important If there were only countably many we could use similar constructions to the earlier case and the countable construction given earlier Since U really is a much richer model than the ones based on finite trac
Download Pdf Manuals
Related Search