Verification of diagnosability based on compositional branching bisimulation

This paper presents an efficient diagnosability verification technique, based on a general abstraction approach. We exploit branching bisimulation including state labels with explicit divergence (BBSD), which preserves the temporal logic property that verifies diagnosability. Furthermore, using compositional abstraction for modular diagnosability verification offers additional state space reduction in comparison to state-of-the-art techniques.