Generalized fair reachability analysis for cyclic protocols: decidability for logical correctness problems

In a previous paper, we generalized the fair reachability notion to cyclic protocols with n⩾2 machines and showed that deadlock detection is decidable for 𝒫, the class of cyclic protocols whose fair reachable state spaces are finite. In this paper, we show that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for class 𝒫 via finite extension of the fair reachable state space. This study shows that for the class 𝒫, our generalized fair reachability analysis technique not only achieves substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a viable state reduction technique