Deciding Detectability for Labeled Petri Nets
For researchers in discrete event systems, this paper provides decidability results for detectability in labeled Petri nets, which are more expressive than finite-state automata, but the results are theoretical and incremental.
This paper investigates the verification of strong and weak detectability for discrete event systems modeled by labeled Petri nets, proving that strong detectability is decidable while weak detectability is undecidable. These results extend detectability verification from finite-state automata to Petri nets and strengthen a result on current-state opacity.
Detectability of discrete event systems (DESs) is a property to determine a priori whether the current and subsequent states can be determined based on observations. In this paper, we investigate the verification of two detectability properties -- strong detectability and weak detectability -- for DESs modeled by labeled Petri nets. Strong detectability requires that we can always determine, after a finite number of observations, the current and subsequent markings of the system, while weak detectability requires that we can determine, after a finite number of observations, the current and subsequent markings for some trajectories of the system. We show that for DESs modeled by labeled Petri nets, checking strong detectability is decidable whereas checking weak detectability is undecidable. Our results extend the existing studies on the verification of detectability from finite-state automata to labeled Petri nets. As a consequence, we strengthen a result on checking current-state opacity for labeled Petri nets.