Diagnosability verification using LTL model checking

DOI10.1007/s10626-022-00360-wzbMath1500.93071OpenAlexW4226241072MaRDI QIDQ2081084

Antonio E. C. da Cunha, Thiago M. Tuxi, Eduardo Vieira Leão Nunes, Lilian Kawakami Carvalho

Publication date: 12 October 2022

Published in: Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10626-022-00360-w

zbMATH Keywords

toolsmodel-checkinglinear temporal logicstatistical analysisdiagnosability

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Temporal logic (03B44)

Uses Software

• REGAL
• TINA
• SPIN
• NuSMV
• UMDES
• DESUMA
• GIDDES
• Supremica

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Diagnosability analysis of patterns on bounded labeled prioritized Petri nets
• Computation of minimal event bases that ensure diagnosability
• Fault detection for discrete event systems using Petri nets with unobservable transitions
• Enumeration and random generation of accessible automata
• Diagnosability of discrete event systems and its applications
• Empirical studies in the size of diagnosers and verifiers for diagnosability analysis
• Robust diagnosis of discrete event systems against intermittent loss of observations
• Coordinated decentralized protocols for failure diagnosis of discrete event systems
• Introduction to Discrete Event Systems
• Distributed Diagnosis of Discrete-Event Systems Using Petri Nets
• Active diagnosis of discrete-event systems
• A polynomial algorithm for testing diagnosability of discrete-event systems
• Handbook of Model Checking
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Diagnosability of discrete-event systems
• Decentralized Prognosis of Failures in Discrete Event Systems
• Maximum Likelihood Failure Diagnosis in Finite State Machines Under Unreliable Observations
• Polynomial-time verification of diagnosability of partially observed discrete-event systems
• Failure Diagnosis of Discrete-Event Systems With Linear-Time Temporal Logic Specifications
• Global and local consistencies in distributed fault diagnosis for discrete-event systems
• Polynomial Time Verification of Decentralized Diagnosability of Discrete Event Systems
• The Complexity of Codiagnosability for Discrete Event and Timed Systems
• Diagnosis of Discrete Event Systems Using Satisfiability Algorithms: A Theoretical and Empirical Study