Deciding detectability for labeled Petri nets

DOI10.1016/J.AUTOMATICA.2019.02.058MaRDI QIDQ1737932zbMATH OpenOpenAlexWikidataFDO

Authors Tomáš Masopust, Xiang Yin

Publication date 24 April 2019

Published in Automatica (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1802.02087

zbMATH Keywords

complexitydetectabilitydecidabilityPetri netsdiscrete event systems

Mathematics Subject Classification ID

Observability (93B07) Discrete event control/observation systems (93C65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

• On detectability of labeled Petri nets and finite automata
• On the Decidability and Complexity of Diagnosability for Labeled Petri Nets
• Analysis of strong and strong periodic detectability of bounded labeled Petri nets
• Marking diagnosability verification in labeled Petri nets
• Codiagnosability Enforcement in Labeled Petri Nets
• Verification of C-detectability using Petri nets
• Decidability of opacity verification problems in labeled Petri net systems
• scientific article; zbMATH DE number 6936874
• Enforcement of Diagnosability in Labeled Petri Nets via Optimal Sensor Selection
• Diagnosability analysis of patterns on bounded labeled prioritized Petri nets

Cites work

• scientific article; zbMATH DE number 3722109 (Why is no real title available?)
• scientific article; zbMATH DE number 6936874 (Why is no real title available?)
• A New Approach for Diagnosability Analysis of Petri Nets Using Verifier Nets
• A unified approach for deciding the existence of certain petri net paths
• Complexity of deciding detectability in discrete event systems
• Decidability of opacity verification problems in labeled Petri net systems
• Deciding detectability for labeled Petri nets
• Delayed Detectability of Discrete Event Systems
• Detectability of Discrete Event Systems
• Generalized detectability for discrete event systems
• Initial-state detectability of stochastic discrete-event systems with probabilistic sensor failures
• ON YEN'S PATH LOGIC FOR PETRI NETS
• Observability of discrete event dynamic systems
• On the Decidability and Complexity of Diagnosability for Labeled Petri Nets
• The problem of determining the weak (periodic) detectability of discrete event systems is PSPACE-complete
• Verification complexity of a class of observational properties for modular discrete events systems
• Verification of detectability in probabilistic finite automata

Cited in

(15)

• Complexity of deciding detectability in discrete event systems
• On verification of D-detectability for discrete event systems
• Path detectability verification for time-dependent systems with application to flexible manufacturing systems
• An improved approach for verifying delayed detectability of discrete-event systems
• Analysis of strong and strong periodic detectability of bounded labeled Petri nets
• On the verification of detectability for timed discrete event systems
• Detectability of labeled weighted automata over monoids
• On detectability of labeled Petri nets and finite automata
• Initial-state detectability and initial-state opacity of unambiguous weighted automata
• A Unified Method to Decentralized State Detection and Fault Diagnosis/prediction of Discrete-event Systems
• The problem of determining the weak (periodic) detectability of discrete event systems is PSPACE-complete
• Deciding Selective Declassification of Petri Nets
• Deciding detectability for labeled Petri nets
• Detectability of networked discrete event systems
• Verification of C-detectability using Petri nets

This page was built for publication: Deciding detectability for labeled Petri nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1737932)