On detectability of labeled Petri nets with inhibitor arcs.

Detectability is a basic property of dynamic systems: when it holds one canuse the observed output signal produced by a system to reconstruct its currentstate.

In this paper, we consider properties of this type in the framework ofdiscrete event systems modeled by Petri nets (a.k.a. place/transition nets). Wefirst study weak detectability and weak approximate detectability. The formerimplies that there exists an evolution of the net such that all correspondingobserved output sequences longer than a given value allow one to reconstructthe current marking (i.e., state). The latter implies that there exists anevolution of the net such that all corresponding observed output sequenceslonger than a given value allow one to determine if the current marking belongsto a given set. We show that the problem of verifying the first property forlabeled place/transition nets with inhibitor arcs and the problem of verifyingthe second property for labeled place/transition nets are both undecidable.

We also consider a property called instant strong detectability which impliesthat for all possible evolutions the corresponding observed output sequenceallows one to reconstruct the current marking. We show that the problem ofverifying this property for labeled place/transition nets is decidable whileits inverse problem is EXPSPACE-hard.