Measuring Time Lag with Nested Preemptions and Resumptions

Controller automata, adopting an unbounded stack, provide sequential execution of a group of timed automata according to various priority policies. When a preemption between two processes is considered, a time lag function is used to transform a timed automaton into one that waits a certain time when preempted by another timed automaton. This paper proposes a static algorithm for timed lag by cloning locations of an original timed automaton. An instantaneous semantics of controller automata is also introduced, in which a time lag happens exactly when the timed automaton is preempted, by giving an upper approximation of latency time. The proposed technology provides convenience for later efficient implementations.