Reachability analysis for communication service specifications described in global state transition rules

The basic properties of reachability analysis for telecommunication service specifications, which are defined by production rules, are discussed. While reachability analyses for conventional specification description is limited to a certain small number of processes so far, we consider an unspecified large number of processes for the first time. This report clarifies the relationship between the number of processes in the system and the size of the set of reachable states defined as subset of global state. It also presents the existence of an upper bound for the set of reachable states and a method of determining the minimum number of processes required to obtain that upper bound. This makes it possible to analyze the reachability of a system for which an infinite number of processes are assumed