On Verification of D-Detectability for Discrete Event Systems

TL;DR

This paper investigates the computational complexity of verifying D-detectability in discrete event systems, establishing that deciding strong periodic D-detectability is PSpace-complete and identifying cases where the problem is tractable.

Contribution

It proves that deciding strong periodic D-detectability is PSpace-complete and shows no polynomial-time algorithm exists unless PSpace=P, also identifying a tractable class of systems.

Findings

Deciding weak D-detectability is PSpace-complete.

Deciding strong periodic D-detectability is PSpace-complete.

No polynomial-time algorithm exists for strong periodic D-detectability even with a single observable event.

Abstract

Detectability has been introduced as a generalization of state-estimation properties of discrete event systems studied in the literature. It asks whether the current and subsequent states of a system can be determined based on observations. Since, in some applications, to exactly determine the current and subsequent states may be too strict, a relaxed notion of D-detectability has been introduced, distinguishing only certain pairs of states rather than all states. Four variants of D-detectability have been defined: strong (periodic) D-detectability and weak (periodic) D-detectability. Deciding weak (periodic) D-detectability is PSpace-complete, while deciding strong (periodic) detectability or strong D-detectability is polynomial (and we show that it is actually NL-complete). However, to the best of our knowledge, it is an open problem whether there exists a polynomial-time algorithm deciding strong periodic D-detectability. We solve this problem by showing that deciding strong periodic D-detectability is a PSpace-complete problem, and hence there is no polynomial-time algorithm unless PSpace = P. We further show that there is no polynomial-time algorithm deciding strong periodic D-detectability even for systems with a single observable event, unless P = NP. Finally, we propose a class of systems for which the problem is tractable.