Diagnosability of fair transition systems

DOI10.1016/j.artint.2022.103725zbMath1491.68107OpenAlexW4223976924MaRDI QIDQ2152493

Viktoria Vozarova, Stefano Tonetta, Marco Gario, Alessandro Cimatti, Marco Bozzano, Benjamin Bittner

Publication date: 8 July 2022

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2022.103725

zbMATH Keywords

diagnosisdiagnosabilitysymbolic model-checkingfair transition systems

Mathematics Subject Classification ID

Reliability, availability, maintenance, inspection in operations research (90B25) Observability (93B07) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• NuSMV
• MathSAT5
• nuXmv
• HyComp

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A game-theoretic approach to fault diagnosis and identification of hybrid systems
• Diagnosability analysis of patterns on bounded labeled prioritized Petri nets
• Fairness of transitions in diagnosability of discrete event systems
• HRELTL: a temporal logic for hybrid systems
• A theory of diagnosis from first principles
• The complexity of reasoning about knowledge and time. I: Lower bounds
• Modalities for model checking: Branching time logic strikes back
• On an optimization problem in sensor selection
• Diagnosability analysis of hybrid systems cast in a discrete-event framework
• Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems
• Accurate Approximate Diagnosability of Stochastic Systems
• FDI(R) for satellites: How to deal with high availability and robustness in the space domain?
• Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
• Counterexample-guided abstraction refinement for symbolic model checking
• Symbolic Fault Tree Analysis for Reactive Systems
• A polynomial algorithm for testing diagnosability of discrete-event systems
• Diagnosability of discrete-event systems
• Optimal sensor selection for discrete-event systems with partial observation
• Polynomial-time verification of diagnosability of partially observed discrete-event systems
• The MathSAT5 SMT Solver
• Verification of Hybrid Automata Diagnosability by Abstraction
• A New Approach for Diagnosability Analysis of Petri Nets Using Verifier Nets
• An automata-theoretic approach to branching-time model checking
• Fault Diagnosis for Timed Automata
• Logic and structure.

This page was built for publication: Diagnosability of fair transition systems