Diagnosability verification using LTL model checking
type: Item
instance of: scholarly article
title: Diagnosability verification using LTL model checking
zbMATH Open document ID: 1500.93071
author: Thiago M. Tuxi
author: Eduardo V. L. Nunes
author: Antonio E. C. da Cunha
author: Lilian Kawakami Carvalho
published in: Discrete Event Dynamic Systems
publication date: 2022-10-12T00:00:00Z
Mathematics Subject Classification ID: 93C65
Mathematics Subject Classification ID: 03B44
zbMATH DE Number: 7600209
zbMATH Keywords: diagnosability
zbMATH Keywords: model-checking
zbMATH Keywords: linear temporal logic
zbMATH Keywords: statistical analysis
zbMATH Keywords: tools
describes a project that uses: Supremica
describes a project that uses: DESUMA
describes a project that uses: GIDDES
describes a project that uses: UMDES
describes a project that uses: NuSMV
describes a project that uses: REGAL
describes a project that uses: TINA
describes a project that uses: SPIN
MaRDI profile type: Publication
full work available at URL: s10626-022-00360-w
OpenAlex ID: W4226241072
cites work: Maximum Likelihood Failure Diagnosis in Finite State Machines Under Unreliable Observations
cites work: Q5322945
cites work: Computation of minimal event bases that ensure diagnosability
cites work: Q3077339
cites work: Enumeration and random generation of accessible automata
cites work: The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
cites work: Fault detection for discrete event systems using Petri nets with unobservable transitions
cites work: Robust diagnosis of discrete event systems against intermittent loss of observations
cites work: Introduction to Discrete Event Systems
cites work: The Complexity of Codiagnosability for Discrete Event and Timed Systems
cites work: Q4804909
cites work: Handbook of Model Checking
cites work: Empirical studies in the size of diagnosers and verifiers for diagnosability analysis
cites work: Coordinated decentralized protocols for failure diagnosis of discrete event systems
cites work: Distributed Diagnosis of Discrete-Event Systems Using Petri Nets
cites work: Diagnosability analysis of patterns on bounded labeled prioritized Petri nets
cites work: Diagnosis of Discrete Event Systems Using Satisfiability Algorithms: A Theoretical and Empirical Study
cites work: A polynomial algorithm for testing diagnosability of discrete-event systems
cites work: Failure Diagnosis of Discrete-Event Systems With Linear-Time Temporal Logic Specifications
cites work: Decentralized Prognosis of Failures in Discrete Event Systems
cites work: Diagnosability of discrete event systems and its applications
cites work: Polynomial Time Verification of Decentralized Diagnosability of Discrete Event Systems
cites work: Diagnosability of discrete-event systems
cites work: Active diagnosis of discrete-event systems
cites work: Global and local consistencies in distributed fault diagnosis for discrete-event systems
cites work: Polynomial-time verification of diagnosability of partially observed discrete-event systems
DOI: 10.1007/S10626-022-00360-W
description: scientific article; zbMATH DE number 7600209