Verification of Detectability Using Petri Nets and Detector

TL;DR

This paper introduces new, more efficient methods using detectors and basis reachability graphs to verify strong detectability properties in bounded labeled Petri nets without exhaustive reachability analysis.

Contribution

The paper proposes novel approaches utilizing detectors and basis reachability graphs to verify detectability in Petri nets more efficiently than existing methods.

Findings

The new methods avoid computing the entire reachability space.

They do not require building the observer.

The approaches are more efficient for verifying detectability.

Abstract

Detectability describes the property of a system to uniquely determine, after a finite number of observations, the current and subsequent states. In this paper, to reduce the complexity of checking the detectability properties in the framework of bounded labeled Petri nets, we use a new tool, which is called detector, to verifying the strong detectability and periodically strong detectability. First, an approach, which is based on the reachable graph and its detector, is proposed. Then, we develop a novel approach which is based on the analysis of the detector of the basis reachability graph. Without computing the whole reachability space, and without building the observer, the proposed approaches are more efficient.