FORMAL VERIFICATION OF A CLASS OF CONCURRENT PROGRAMS.

A program system including array variables for verification of concurrent programs is defined, and the decision problem for invariance of a predicate P given in terms of program variables is discussed in order to determine whether it meets certain requirements. A sufficient condition is given to determine the invariance of P in this system. Then, as an example of concurrent programs in that decidable class, an abstract transmission control procedure is considered and it is shown that the proof for invariance of the predicate, which is the object of verification, can formally be discussed in the framework of the decidable class mentioned in this paper. Furthermore, it is shown that problem of such dynamical properties as the possibility of correct execution of concurrent programs is undecidable even for simple cases.