Detectability is a basic property of dynamic systems: when it holds an observer can use the current and past values of 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 infinite observed output sequence of the system such that each prefix of the output sequence with length greater than a given value allows an observer to determine if the current state belongs to a given set. We prove that the problem of verifying this property is undecidable for labeled Petri nets, and PSPACE-complete for finite automata. We also consider one new concept called eventual strong detectability. The new property implies that for each possible infinite observed output sequence, there exists a value such that each prefix of the output sequence with length greater than that value allows reconstructing the current state. We prove that for labeled Petri nets, the problem of verifying eventual strong detectability is decidable and EXPSPACE-hard, where the decidability result holds under a mild promptness assumption. For finite automata, we give a polynomial-time verification algorithm for the property. In addition, we prove that strong detectability is strictly stronger than eventual strong detectability for labeled Petri nets and even for deterministic finite automata.

On detectability of labeled Petri nets and finite automata

Zhang K.;Giua A.
2020-01-01

Abstract

Detectability is a basic property of dynamic systems: when it holds an observer can use the current and past values of 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 infinite observed output sequence of the system such that each prefix of the output sequence with length greater than a given value allows an observer to determine if the current state belongs to a given set. We prove that the problem of verifying this property is undecidable for labeled Petri nets, and PSPACE-complete for finite automata. We also consider one new concept called eventual strong detectability. The new property implies that for each possible infinite observed output sequence, there exists a value such that each prefix of the output sequence with length greater than that value allows reconstructing the current state. We prove that for labeled Petri nets, the problem of verifying eventual strong detectability is decidable and EXPSPACE-hard, where the decidability result holds under a mild promptness assumption. For finite automata, we give a polynomial-time verification algorithm for the property. In addition, we prove that strong detectability is strictly stronger than eventual strong detectability for labeled Petri nets and even for deterministic finite automata.
2020
Labeled Petri net; Finite automaton; Weak approximate detectability; Eventual strong detectability; Decidability; Complexity
File in questo prodotto:
File Dimensione Formato  
20deds.pdf

accesso aperto

Descrizione: articolo online
Tipologia: versione editoriale (VoR)
Dimensione 1.89 MB
Formato Adobe PDF
1.89 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/299243
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 18
  • ???jsp.display-item.citation.isi??? 20
social impact