Dealing with Zero-Time Transitions in Axiom Systems

In the modalization 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 appeal of the zero-time transition abstraction, yet maintains simplicity and generality in its use. The approach is based on considering zero-time transitions as occurring in an infinitesimal, yet nonnull time. The adopted notation is borrowed from nonstandard 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.