Decentralized Supervisory Control of Discrete Event Systems for Bisimulation Equivalence

TL;DR

This paper develops a formal automata-based framework for decentralized control of nondeterministic discrete event systems, ensuring bisimulation equivalence with specifications, extending traditional supervisory control results to finer behavioral equivalences.

Contribution

It introduces three architectures for decentralized bisimulation control and derives necessary and sufficient conditions for supervisor existence, extending supervisory control theory to bisimulation.

Findings

Conditions for decentralized bisimilarity supervisor existence are established.

Verification of conditions can be performed with exponential complexity.

Bisimilarity supervisors can be synthesized when conditions are met.

Abstract

In decentralized systems, branching behaviors naturally arise due to communication, unmodeled dynamics and system abstraction, which can not be adequately captured by the traditional sequencing-based language equivalence. As a finer behavior equivalence than language equivalence, bisimulation not only allows the full set of branching behaviors but also explicitly specifies the properties in terms of temporal logic such as CTL* and mu-calculus. This observation motivates us to consider the decentralized control of discrete event systems (DESs) for bisimulation equivalence in this paper, where the plant and the specification are taken to be nondeterministic and the supervisor is taken to be deterministic. An automata-based control framework is formalized, upon which we develop three architectures with respect to different decision fusion rules for the decentralized bisimilarity control, named a conjunctive architecture, a disjunctive architecture and a general architecture. Under theses three architectures, necessary and sufficient conditions for the existence of decentralized bisimilarity supervisors are derived respectively, which extend the traditional results of supervisory control from language equivalence to bisimulation equivalence. It is shown that these conditions can be verified with exponential complexity. Furthermore, the synthesis of bisimilarity supervisors is presented when the existence condition holds.