Some Properties of Reactive FIFFO Automata

Abstract:

We are interested in the verification of real-time systems modelled with Reactive FIFFO (First In First Fireable Out) Automata. This model provides with the ability of memorizing events when they must not be taken into account at their occurrence date. We aim at deciding the boundedness of the queue.

Keywords:

Real-time systems, Reactive Fiffo Automata, Event memorizing, Boundedness.

Download:

[ps.gz | pdf]