[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

about the recursive process

I am confused by the definition of recursive processes in PVS.  Is there anybody could give me some good ideas? Let's me make a example:
P = a -> b -> P
this is a recursive process of CSP. One of methods to solve this problem is to use the parametric process and the least fixed point.
X: VAR [U -> process]
F: VAR [[U->process] -> [U->process]]
F(X)(x)= a>>b>>X(x+1)
then P:[U->process] = mu(H)
This method is efficient only when we deal with the simply process like verifying the process P is a subset of specific specification. But when meet the little complex situation, it is difficult. For example, there are two group of processes:
P(i) = a->b->c->P(i)      Q(i)=c->Q(i)
First, we get the interleaving of all the P(i) and Q(i) respectively.
Interleave(P)   Interleave(Q)
then make them synchronized. Interleave(P) || Interleave(Q)
So, is it possible we give up the parametric processes to define the recursive process in PVS, is it easier?