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

Re: about the recursive process

   I am confused by the definition of recursive processes in PVS.
   Is there anybody could give me some good ideas? 

One way to circumvent a recursive definition is to formalize your
processes as coalgebras, ie. function of the form 

   State -> Observation_type[State]

This has been done several times (even in PVS), see

Modelling process calculi with PVS, D. Schamschurko, 
	CMCS 98, ENTCS 11

A coalgebraic introduction into CSP, U Wolter,
	CMCS 99, ENTCS 19

Process Calculi a al Bird-Meertens, L S Barbose,
	CMCS 01, ENTCS 44.1

CoCASL at Work - Modelling Process Algebra,
	Mossakowski,Roggenbach, Schroeder, CMCS 03, ENTCS 82.1

The ENTCS series is online available at