도달가능성 분석에서 유한 및 결정적 DEVS의 전이 시스템 의미

Transition System Semantics of Finite and Deterministic DEVS in Reachability Analysis

Reachability analysis of DEVS models has been realized by using model checkers for timed automata (TA) through the conversion of them to TA;or by finding verifiable subclasses of DEVS with the development of analysis methods for them. In this paper;the author studies the semantics of finite and deterministic DEVS (FD-DEVS);which is a verifiable subclass of DEVS;from a viewpoint of a low-level representation of automata;transition systems;so that an atomic FD-DEVS model is interpreted;with respect to reachability analysis;as a transition system. This would mean that;although an analysis method for FD-DEVS was already proposed;reachability of FD-DEVS models can be also analyzed by methods of TA.