Abstract
In the modelization of time-dependent systems it is often useful to use the abstraction of zero-time transitions, i.e., changes
of system state that occur in a time that can be neglected with respect to the whole dynamics of system evolution. Such an
abstraction, however, sometimes generates critical situations in the formal system analysis. This may lead to limitations
or unnatural use of such formal analysis. In this paper we present an approach that keeps the intuitive appealing of the zero-time
transition abstraction yet maintaining simplicity and generality in its use. The approach is based on considering zero-time
transitions as occurring in an infinitesimal, yet non-null time. The adopted notation is borrowed from non-standard analysis.
The approach is illustrated through Petri nets as a case of state machines and TRIO as a case of logic-based assertion language,
but it can be easily applied to any formal system dealing with states, time, and transitions.
[download the pdf file] [DOI]