Analysis of Arbitrarily Large Networks of Discrete-Event Systems

Many engineering systems can be usefully modelled as networks of interacting, isomorphic, finite-state discrete-event systems. Examples include communication and transportation networks. For practical purposes, the number of subsystems is often arbitrary. In such cases, key problems of analysis are generally undecidable; however, inductive semidecision procedures can be formulated for checking whether networks of arbitrary size are equivalent to networks of bounded size. The appropriate notion of equivalence may vary, depending on the properties being analyzed. We examine a range of possible equivalences, identify system properties that they preserve, and show that semidecision procedures exist for checking these equivalences. On the other hand, we show that equivalence of networks to networks of bounded size is undecidable for a broad range of process equivalences, even for the simple network topologies of rings and line segments.