# Verification of C-detectability Using Petri Nets

## TL;DR

This paper introduces a relaxed form of detectability called C-detectability for Petri nets, enabling efficient verification of crucial state distinguishability without exhaustive reachability analysis.

## Contribution

It defines four types of C-detectability within Petri nets and develops efficient verification methods based on basis markings, avoiding full reachability space computation.

## Key findings

- Four types of C-detectability are formally defined.
- Verification methods are more efficient than traditional approaches.
- Approaches do not require enumerating all markings.

## Abstract

Detectability describes the property of an system whose current and the subsequent states can be uniquely determined after a finite number of observations. In this paper, we relax detectability to C-detectability that only requires a given set of crucial states can be distinguished from other states. Four types of C-detectability: strong C-detectability, weak C-detectability, periodically strong C-detectability, and periodically weak C-detectability are defined in the framework of labeled Petri nets, which have larger modeling power than finite automata. Moreover, based on the notion of basis markings, the approaches are developed to verify the four C-detectability of a bounded labeled Petri net system. Without computing the whole reachability space and without enumerating all the markings consistent with an observation, the proposed approaches are more efficient.