Synchronous Composition of Finite Interval Automata

In this work, we study the class of real-time discrete-event systems modeled by finite interval automata, i.e., a finite state automaton where each transition is labeled by an event and an interval. The class of finite interval automata is interpreted over discrete time models and corresponds exactly to the class of finite tick automata. An interval domain construction of the synchronous product of finite interval automata is provided that exactly encodes the synchronous product in the tick domain. This avoids explicit enumeration of clock ticks that is required by the timed discrete-event systems and finite tick automata formalism. To increase the expressive power of the finite interval automata, we also distinguish preempting transitions from non-preempting transitions. As a result, each timed discrete-event system can be encoded using a finite interval automaton.