Weak invariant simulation and analysis of parameterized networks

Abstract

Multi-process networks figure in many engineering applications such as communication networks, transportation networks, manufacturing and logistic systems, and computer hardware and software. Parameterized discrete event systems provide a convenient means of modeling such networks when the number of subprocesses is arbitrary, unknown or time-varying. Unfortunately, some key properties of these networks, such as nonblocking and deadlock-freedom, are undecidable. Moreover, mathematical tools supporting analysis of these networks are limited. This thesis introduces a novel mathematical notion, weak invariant simulation and proposes an efficient method to check whether a finite-state generator weakly invariantly simulates another finite-state generator with respect to a specific subalphabet. This new simulation relation is first used to define a tractable subclass of parameterized ring networks of isomorphic subprocesses in which deadlock-freedom is decidable. Within this framework, a procedure is given to determine the reachable deadlocked states of the network. The effectiveness of the procedure is demonstrated by the deadlock analysis of a version of the dining philosophers problem.

To generalize the results on ring networks, we consider a network consisting of several linear parameterized sections but exhibiting a branching topology. To model these networks we introduce Generalized Parameterized Discrete Event Systems (GPDES). The difficulty in analysis of a GPDES is the fact that some of the subprocesses interact with several parameterized sections of the network. Hence the analysis proposed in this thesis involves careful study of interaction among different branches of the network. Here again, we use `weak invariant simulation' to limit the behavior of subprocesses of the network. Then we investigate interactions among different components of the network, using a dependency graph. The dependency graph is a directed graph developed to characterize reachable partial deadlocks caused by generalized circular waits in the proposed GPDES. Our results implicitly characterize reachable generalized circular waits as a language accepted by a finite automaton. Our framework allows for modeling and analysis of new parameterized problems. We investigated deadlock in a large-scale factory as an illustrative example.