Rational Time-Advance DEVS (RTA-DEVS)

摘要

This paper introduces a new extension to the DEVS formalism, called Rational Time-Advance DEVS. The basic idea of this new formalism is to permit modeling the behavior of systems that can be modeled by classical DEVS; however, RTA-DEVS models could be formally checked with standard model-checking algorithms and tools. In order to do so, we introduce a procedure to create Timed Automata models that are behaviorally equivalent to the original RTA-DEVS models. This therefore, enables the use of the available TA tools and theories for formal model checking.