Hello,
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?
Kun
