Title :
Reachability Graph of Finite and Deterministic DEVS Networks
Author :
Hwang, Moon Ho ; Zeigler, Bernard P.
Author_Institution :
Dept. of Electr. & Comput. Eng., Univ. of Arizona, Tucson, AZ, USA
fDate :
7/1/2009 12:00:00 AM
Abstract :
This paper shows how to generate a finite-vertex graph, called a reachability graph for discrete-event system specification (DEVS) network. The reachability graph is isomorphic to a given original DEVS network in terms of behavior but the number of vertices as well as the number of edges of the reachability graph are finite.
Keywords :
formal specification; reachability analysis; deterministic DEVS networks; discrete-event system specification; finite DEVS networks; finite-vertex graph; reachability graph; Discrete-event system specification (DEVS); finite-vertex reachability graph; time abstraction; verification;
Journal_Title :
Automation Science and Engineering, IEEE Transactions on
DOI :
10.1109/TASE.2009.2021352
