View article

If a system is built from a large number of identical finite-state processes, it seems intuitively obvious that, with the help of" a little induction", the verification of such a system can be reduced to a finite-state problem. The difficulty is to find the right form of" a little induction". There have been several attempts to address this problem in the context of model-checking [CGBS6],[CGS7],[GSS7]. In very general terms (see Section 6 for more details), the approach is to find ways of proving that if a process satisfies a fornmla, then the n-fold parallel composition of this process with itself still satisfies the same (or a related) formula. This approach makes some interesting verifications possible. However, it has its limits and usually requires the implementation of special purpose tools. In this paper, we propose an alternative approach. It is an attempt to make the" little induction" explicit and simple. If one wants to prove that some …