Reachability analysis for communication service specification descriptions in global state transition rules

Abstract This paper discusses fundamental characteristics in reachability analysis of communication service specifications defined by means of production rules. In the conventional service specifications, reachability has been analyzed within a finite number of communication processes. However, it is necessary to deal with infinite processes to verify state reachability of the global transition description of the production rules. If the reachability state as a reachable subglobal state constructed with a number of processes is defined, the size of the reachability state set depends on the number of processes at the initial state. In general, the system is analyzed on the assumption of an infinitive number of processes to verify reachability. This paper presents the relationship between the size of the reachable set and the number of processes in the system. It also shows the existence of the upper bound of the reachable state set and a method to obtain the minimum number of processes that gives the upper bound of the reachable set. This study makes it possible to analyze the reachability of an infinite number of processes by a reachability problem of finite number of processes.