On detectability of labeled Petri nets and finite automata
share
Detectability is a basic property of dynamic systems: when it holds one can use the observed output signal produced by a system to reconstruct its current state. In this paper, we consider properties of this type in the framework of discrete event systems modeled by labeled Petri nets and finite automata. We first study weak approximate detectability. This property implies that there exists an evolution of the system such that each corresponding observed output sequence with length greater than a given value allows one to determine if the current state belongs to a given set. We show that the problem of verifying this property is undecidable for labeled Petri nets, and PSPACE-complete for finite automata. We also consider two new concepts called instant strong detectability and eventual strong detectability. The former property implies that for each possible evolution the corresponding observed output sequence allows one to reconstruct the current state. The latter implies that for each possible evolution, there exists a value such that each corresponding observed output sequence with length greater than than that value allows one to reconstruct the current state. We show that for labeled Petri nets, the problems of verifying these two properties are both decidable and EXPSPACE-hard; while for finite automata, both properties can be verified in polynomial time. In addition, we show that strong detectability in the literature is strictly stronger than eventual strong detectability, but strictly weaker than instant strong detectability, for both finite automata and labeled Petri nets. In particular for deterministic finite au- tomata, eventual strong detectability is equivalent to strong detectability.
READ FULL TEXT