Detection of summative global predicates

In distributed programs, we usually keep some global predicates from being satisfied to make it easy to run the programs correctly. A common type of global predicates are: the total number of certain tokens in the whole distributed system is always the same or in specific ranges. In this paper, we call this summative predicates, classified into the following four: (1) at some global state of the system, N≠K, (2) N<K (or N⩽K), (3) N>K (or N⩾K), and (4) N=K, where N is the total number of tokens and K is a constant. This paper investigates the methods of detecting various summative global predicates. The first class of summative predicates are trivial to detect by simply checking each message. For the second class of summative predicates, B. Groselj (1993) and V.K. Garg (1995) solved the problem by reducing the problem to a maximum network flow problem. In this paper, we propose an elegant technique, called normalization, to allow the second and third classes of summative predicates to be solved by also reducing the problem to a maximum network flow problem. For the fourth class of summative predicates, we prove that it is an NP-complete problem