Opacidade de sistemas a eventos discretos modelados por uma classe de autômatos temporizados

This paper addresses the problem of language opacity for a class of discrete-event systems whose transitions occur within some known time interval after the event becomes enabled. For this purpose, a new class of timed automata is proposed, the so-called time-interval automata, in which a time interval is associated with each event that labels a transition. For such automata, the operations of complement, projection and product are redefined without using refinement by partition, as usually used in the literature. The usual language-based definition of opacity is extended to this class of automata and an algorithm for its verification is proposed.