Bisimilarity Enforcing Supervisory Control for Deterministic Specifications

TL;DR

This paper develops a framework for controlling nondeterministic discrete event systems to ensure they behave exactly as deterministic specifications through bisimilarity, providing verification algorithms and synthesis methods.

Contribution

It introduces a new notion of synchronous simulation-based controllability and offers polynomial algorithms for supervisor synthesis and maximal permissive sub-specification generation.

Findings

A necessary and sufficient condition for bisimilarity enforcement is established.

Polynomial-time algorithms are developed for verification and supervisor synthesis.

Methods for synthesizing maximal permissive sub-specifications are proposed.

Abstract

This paper investigates the supervisory control of nondeterministic discrete event systems to enforce bisimilarity with respect to deterministic specifications. A notion of synchronous simulation-based controllability is introduced as a necessary and sufficient condition for the existence of a bisimilarity enforcing supervisor, and a polynomial algorithm is developed to verify such a condition. When the existence condition holds, a supervisor achieving bisimulation equivalence is constructed. Furthermore, when the existence condition does not hold, two different methods are provided for synthesizing maximal permissive sub-specifications.