部分観測離散事象システムに関する性質の多くは，その検証のための計算量がオートマトンモデルの状態数に依存するため，規模の大きなシステムでは検証が困難になる可能性がある.本稿では，部分観測離散事象システムの幾つかの性質に関して，対象システムのオートマトンモデルを抽象化し，抽象化モデルを用いた検証が可能であるための十分条件を導出する.%For partially observed discrete event systems, the computational complexity for their verification generally depends on the number of states of their automata models. This fact implies that it is often difficult to perform verification of large-scale systems. In this paper, we use abstraction of partially observed discrete event systems, and present sufficient conditions under which some of their properties can be verified on the abstracted models.
展开▼
