Invariant weak simulation and analysis of parameterized networks

Communicating multi-process networks appear in many real-life applications. Parameterized discrete event systems provide a convenient way of modeling these networks. Unfortunately, some key problems such as checking solvability of the nonblocking synthesis problem and checking satisfaction of a temporal property in parameterized networks are undecidable. In this paper, we consider parameterized ring networks and introduce a new framework for blocking analysis of such networks. To render the blocking analysis tractable, we restrict the interactions between processes. The structural assumptions are formulated in terms of a new mathematical relation: invariant weak simulation of one process by another. Our assumptions serve to ensure that while both immediate neighbors may prevent a process from executing shared events, only one neighbor can permanently prevent an event from occurring; in that sense, control only flows around the ring in one direction. We prove that our assumptions have this desired result. The effectiveness of the proposed framework is demonstrated by analysis of a version of the dining philosophers problem.