Abstraction-Based Verification for Partially Observed Discrete Event Systems

Several properties including observability, normality, diagnosability, and prognosability (predictability) have been proposed for control/diagnosis of partially observed discrete event systems. Although these properties can be verified in polynomial time, their verification may be computationally infeasible for large-scale systems. To reduce the computational effort, abstraction-based verification of diagnosability has been studied in literature. The purpose of this paper is to complement this existing result by presenting conditions under which observability, normality, and prognosability can be verified based on the abstracted models. As a result, diagnosability and prognosability can be verified under the same conditions. Furthermore, observability and normality can be verified under weaker conditions.