Weak Invariant Simulation and Its Application to Analysis of Parameterized Networks

作者：Zibaeenejad M H^*; Thistle J G

来源：IEEE Transactions on Automatic Control, 2014, 59(8): 2024-2037.

DOI：10.1109/TAC.2014.2315311

• Automata
• discrete-event systems
• parameterized systems
• process algebra
• supervisory control

Multi-process networks figure in many engineering applications. 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 paper introduces a novel mathematical notion, weak invariant simulation, which is adapted to the analysis of synchronous products of discrete event systems. Furthermore, it 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 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.

• 出版日期2014-8